feat(Order/Completion): embed a linear order into a dense and complete linear order

[AntoineChambert-Loir]

The aim of the PR is to prove the following theorem that will be used as an input to Sion.DMCompletion.exists_isSaddlePointOn :
If β is any linear order, then there exists a complete and dense linear order γ together with a continuous embedding ι : β ↪o γ (for the order topologies on β and γ).

Meanwhile, the PR also records various instances about dense orders and lemmas regarding the Dedekind MacNeille completion and lexicographic orders.

---

[github-actions]

PR summary cb39573f93

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.Order.Completion (new file)	858

---

Declarations diff

+ DedekindCut.continuous_principal
+ Fill
+ continuous_some
+ exists_dense_continuous_completion
+ instance : DenselyOrdered (Fill α)
+ instance : TopologicalSpace (Fill α) := Preorder.topology _
+ instance [DenselyOrdered α] : DenselyOrdered (DedekindCut α)
+ instance [Preorder α] [Preorder β] [NoMaxOrder β] [DenselyOrdered β] :
+ instance [Preorder α] [Preorder β] [NoMinOrder β] [DenselyOrdered β] :
+ instance [TopologicalSpace α] [OrderTopology α] : OrderTopology (Fill α)
+ le_principal_iff
+ lt_iff_exists
+ lt_iff_exists'
+ lt_principal_iff
+ principal_le_iff
+ principal_lt_iff
+ some

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[vihdzp]

What's the theorem you're trying to prove? Every linear order with the order topology embeds via a continuous map into a dense complete linear order?

[AntoineChambert-Loir]

Yes, but I need that embedding to be continuous for the order topologies. Then the lex product with Q doesn't work, and I believe i'll have to fill the holes but nothing more. (I updated the above description.)

[vihdzp]

I believe Dedekind.principal should always be continuous. You should be able to prove this by showing principal ⁻¹' Iio x = ⋃ y ∈ x.left, Iio (principal y), and likewise for Ioi. Also, the Dedekind completion of a dense order is dense. So that reduces the problem to embedding a linear order into a dense linear order continuously.

[vihdzp]

Embedding α into α ×ₗ ℚ doesn't work directly, but I think you can salvage it by taking a subtype instead. Say that your embedding maps x into toLex (x, 0). My idea is this: if x does not have a predecessor, remove all elements toLex (x, y) with y < 0 from the subtype. If x has no successor, remove all elements toLex (x, y) with 0 < y. I believe this subtype of α ×ₗ ℚ should be dense, and the embedding fun x ↦ toLex (x, 0) will be continuous.

In other words, you're adding a copy of ℚ in between any two consecutive elements.

[AntoineChambert-Loir]

Exactly, that's what I meant with “filling the holes”.

[AntoineChambert-Loir]

I find it easier (the formalization will say so, or not) to define an adequate Sigma type.

[vihdzp]

I think everything outside of Order.Fill and the continuous_principal theorem would make a good self-contained PR.

[vihdzp]

I'll try out my own formalization of this order, if it's any simpler than this I'll let you know.

[vihdzp]

This is one fourth the length of your code :)

/-
Copyright (c) 2026 Violeta Hernández Palacios. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Violeta Hernández Palacios, Antoine Chambert-Loir
-/
module

public import Mathlib.Data.Prod.Lex
public import Mathlib.Order.SuccPred.Limit
public import Mathlib.Topology.Order.Basic

import Mathlib.Algebra.Order.Field.Basic

@[expose] public section

namespace Order

variable {α : Type*} [LinearOrder α]

/-- A dense linear order into which α embeds continuously, formed by "filling in" the blanks. -/
abbrev Fill (α : Type*) [LinearOrder α] : Type _ :=
  {x : α ×ₗ ℚ //
    (IsSuccPrelimit (ofLex x).1 → 0 ≤ (ofLex x).2) ∧
    (IsPredPrelimit (ofLex x).1 → (ofLex x).2 ≤ 0) }

namespace Fill

instance [TopologicalSpace α] [OrderTopology α] : TopologicalSpace (Fill α) :=
  Preorder.topology _

instance [TopologicalSpace α] [OrderTopology α] : OrderTopology (Fill α) :=
  ⟨rfl⟩

/-- A continuous embedding of `α` into `Fill α`. -/
def some : α ↪o Fill α where
  toFun x := ⟨toLex (x, 0), by simp⟩
  inj' _ := by simp
  map_rel_iff' := by simp [Prod.Lex.toLex_le_toLex']

instance : DenselyOrdered (Fill α) where
  dense := by
    simp only [ofLex_toLex, Subtype.forall, Prod.Lex.lt_iff, Subtype.mk_lt_mk,
      Lex.forall, Prod.forall]
    rintro x q ⟨hx₁, hx₂⟩ y r ⟨hy₁, hy₂⟩ (h | ⟨rfl, h⟩)
    · by_cases hx : IsPredPrelimit x
      · obtain ⟨z, hz, hz'⟩ := hx.lt_iff_exists_lt.1 h
        use some z
        simp [some, Prod.Lex.lt_iff, hz', hz]
      obtain ⟨s, hs⟩ := exists_gt (max 0 q)
      rw [max_lt_iff] at hs
      refine ⟨⟨toLex (x, s), ?_⟩, ?_⟩
      · simp [hx, hs.1.le]
      · simp [Prod.Lex.lt_iff, hs.2, h]
    · obtain ⟨s, hs, hs'⟩ := exists_between h
      refine ⟨⟨toLex (x, s), ?_⟩, ?_⟩
      · grind [ofLex_toLex]
      · simp [Prod.Lex.lt_iff, hs, hs']

theorem continuous_some [TopologicalSpace α] [OrderTopology α] : Continuous (X := α) some := by
  simp only [OrderTopology.continuous_iff, ofLex_toLex, Subtype.forall, Lex.forall, Prod.forall]
  refine fun x q ⟨hx₁, hx₂⟩ ↦ ⟨?_, ?_⟩
  · obtain hq | hq := le_or_gt 0 q
    · convert isOpen_Ioi (a := x)
      ext
      simp [some, Prod.Lex.lt_iff, hq.not_gt]
    · obtain ⟨y, hy⟩ := (not_isSuccPrelimit_iff_exists_covBy _).1 <| mt hx₁ hq.not_ge
      convert isOpen_Ioi (a := y)
      ext
      simpa [some, Prod.Lex.lt_iff, hq, le_iff_lt_or_eq] using hy.le_iff_lt_right
  · obtain hq | hq := le_or_gt q 0
    · convert isOpen_Iio (a := x)
      ext
      simp [some, Prod.Lex.lt_iff, hq.not_gt]
    · obtain ⟨y, hy⟩ := (not_isPredPrelimit_iff_exists_covBy _).1 <| mt hx₂ hq.not_ge
      convert isOpen_Iio (a := y)
      ext
      simpa [some, Prod.Lex.lt_iff, hq, le_iff_lt_or_eq] using hy.le_iff_lt_left

end Fill
end Order

[AntoineChambert-Loir]

It's shorter but it does less, although this “less” (holes, etc.) might be uninteresting, and I'm not so happy with the going through Lex, I feel it unnatural.

[AntoineChambert-Loir]

I think everything outside of Order.Fill and the continuous_principal theorem would make a good self-contained PR.
What about Order.Hole?

[vihdzp]

It's shorter but it does less, although this “less” (holes, etc.) might be uninteresting, and I'm not so happy with the going through Lex, I feel it unnatural.

What else do you need it to do? Isn't the core result "any linear order embeds continuously into a dense linear order"?

[AntoineChambert-Loir]

I'm more interested into formalizing the how and the why than the what. It's OK, the core result is there.

[vihdzp]

Both of our constructions are ultimately isomorphic, so I don't see what distinction you're making.

[ADedecker]

I spent way too long trying to build something withe the flexibility of Antoine's approach as well as the conciseness of Violeta's, but this is not a huge success.

One thing to note is that Antoine's construction also works for densifying a partial order, as long as the order relation on holes compares both the left and the right components (which is still more natural, and in the linearly ordered case it's the same).

I think a reasonable middle ground (to keep some flexibility while still allowing for a more direct approach) would be to fill all holes with a single order. Then I would define Fill in the same way Antoine does (an inductive type is probably more natural to use), but pull back the order relation from an appropriate Lex (which means that you get most properties for free, except for continuity which is really specific to the situation).

How does this sound ? Antoine, do you have any reason to believe that the flexibility of putting a different order at different holes could matter for some application ?

[vihdzp]

One thing to note is that Antoine's construction also works for densifying a partial order.

The theorem that any order embeds in a dense order (not necessarily continuously) is trivial, since you can just take the lex product with the rationals (or any other dense nonempty order). The key property here is continuity, but the order topology doesn't really make sense in a partial order (it is well-defined, but rarely if ever the topology you actually want to put on it).

[vihdzp]

I'm not all too comfortable with having [TopologicalSpace (DedekindCut α)] [OrderTopology (DedekindCut α)] as assumptions to a theorem. But other than that, this LGTM.