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

Mathlib.lean

@@ -7750,6 +7750,7 @@ public import Mathlib.Topology.Order.Bornology
 public import Mathlib.Topology.Order.Category.AlexDisc
 public import Mathlib.Topology.Order.Category.FrameAdjunction
 public import Mathlib.Topology.Order.Compact
+public import Mathlib.Topology.Order.Completion
 public import Mathlib.Topology.Order.CountableSeparating
 public import Mathlib.Topology.Order.DenselyOrdered
 public import Mathlib.Topology.Order.ExtendFrom

Mathlib/Data/Prod/Lex.lean

@@ -201,6 +201,37 @@ instance [Preorder α] [Preorder β] [DenselyOrdered α] [DenselyOrdered β] :
     · obtain ⟨c, h₁, h₂⟩ := exists_between h
       exact ⟨(a, c), right _ h₁, right _ h₂⟩
 
+instance [Preorder α] [Preorder β] [NoMinOrder β] [DenselyOrdered β] :
+    DenselyOrdered (α ×ₗ β) where
+  dense x y h := by
+    have this (x : α ×ₗ β) : ∃ a t, x = toLex (a, t) := ⟨x.1 , x.2, rfl⟩
+    rcases this x with ⟨a, t, rfl⟩
+    rcases this y with ⟨b, u, rfl⟩
+    simp only [Prod.Lex.toLex_lt_toLex] at h
+    rcases h with (h | h)
+    · obtain ⟨v, hv⟩ := exists_lt u
+      use toLex (b, v)
+      simp [Prod.Lex.toLex_lt_toLex, h, hv]
+    · obtain ⟨v, htv, hvu⟩ := DenselyOrdered.dense t u h.2
+      use toLex (a, v)
+      simp [Prod.Lex.toLex_lt_toLex, h.1, htv, hvu]
+
+@[to_dual existing]
+instance [Preorder α] [Preorder β] [NoMaxOrder β] [DenselyOrdered β] :
+    DenselyOrdered (α ×ₗ β) where
+  dense x y h := by
+    have this (x : α ×ₗ β) : ∃ a t, x = toLex (a, t) := ⟨x.1 , x.2, rfl⟩
+    rcases this x with ⟨a, t, rfl⟩
+    rcases this y with ⟨b, u, rfl⟩
+    simp only [Prod.Lex.toLex_lt_toLex] at h
+    rcases h with (h | h)
+    · obtain ⟨v, hv⟩ := exists_gt t
+      use toLex (a, v)
+      simp [Prod.Lex.toLex_lt_toLex, h, hv]
+    · obtain ⟨v, htv, hvu⟩ := DenselyOrdered.dense t u h.2
+      use toLex (a, v)
+      simp [Prod.Lex.toLex_lt_toLex, h.1, htv, hvu]
+
 instance noMaxOrder_of_left [Preorder α] [Preorder β] [NoMaxOrder α] : NoMaxOrder (α ×ₗ β) where
   exists_gt := by
     rintro ⟨a, b⟩

Mathlib/Order/Completion.lean

@@ -105,6 +105,16 @@ theorem principal_le_principal {a b : α} : principal a ≤ principal b ↔ a 
 theorem principal_lt_principal {a b : α} : principal a < principal b ↔ a < b := by
   simp [lt_iff_le_not_ge]
 
+lemma principal_le_iff {a : α} {c : DedekindCut α} :
+    principal a ≤ c ↔ a ∈ c.left := by
+  simp only [← extent_subset_extent_iff, left_principal]
+  exact ⟨fun h ↦ h self_mem_Iic, fun h y hy ↦ mem_extent_of_rel_extent hy h⟩
+
+lemma le_principal_iff {a : α} {c : DedekindCut α} :
+    c ≤ principal a ↔ a ∈ c.right := by
+  simp only [← intent_subset_intent_iff, right_principal]
+  exact ⟨fun h ↦ h self_mem_Ici, fun h _y hy ↦ mem_intent_of_intent_rel hy h⟩
+
 /-- We can never have a computable decidable instance, for the same reason we can't on `Set α`. -/
 noncomputable instance : DecidableLE (DedekindCut α) :=
   Classical.decRel _
@@ -205,10 +215,47 @@ noncomputable instance : LinearOrder (DedekindCut α) where
   le_total := total_of _
   toDecidableLE := inferInstance
 
+/-- Use `DedekindCut.lt_iff_exists'` for a version with `<` and `≤` swapped -/
+theorem lt_iff_exists {a b : DedekindCut α} :
+    a < b ↔ ∃ c, a < principal c ∧ principal c ≤ b := by
+  refine ⟨fun h ↦ ?_, fun ⟨c, hca, hcb⟩ ↦ hca.trans_le hcb⟩
+  rw [← extent_ssubset_extent_iff, Set.ssubset_iff_exists] at h
+  simpa [← not_le, principal_le_iff, and_comm] using h.2
+
+/-- Variant of `DedekindCut.lt_iff_exists` with `<` and `≤` swapped -/
+theorem lt_iff_exists' {a b : DedekindCut α} :
+    a < b ↔ ∃ c, a ≤ principal c ∧ principal c < b := by
+  refine ⟨fun h ↦ ?_, fun ⟨c, hca, hcb⟩ ↦ lt_of_le_of_lt hca hcb⟩
+  rw [← intent_ssubset_intent_iff, Set.ssubset_iff_exists] at h
+  simpa [← not_le, le_principal_iff] using h.2
+
 noncomputable instance : CompleteLinearOrder (DedekindCut α) where
   __ := (inferInstance : LinearOrder _)
   __ := (inferInstance : CompleteLattice _)
   __ := LinearOrder.toBiheytingAlgebra _
 
+instance [DenselyOrdered α] : DenselyOrdered (DedekindCut α) where
+  dense a b h := by
+    obtain ⟨c, hac, hcb⟩ := lt_iff_exists.mp h
+    obtain ⟨d, had, hdc⟩ := lt_iff_exists'.mp hac
+    simp only [principal_lt_principal] at hdc
+    obtain ⟨u, _, _⟩ := DenselyOrdered.dense d c hdc
+    exact ⟨principal u, had.trans_lt (by simpa), hcb.trans_lt' (by simpa)⟩
+
+theorem principal_lt_iff {a : α} {c : DedekindCut α} :
+    principal a < c ↔ ∃ b ∈ c.left, a < b := by
+  rw [← not_le, le_principal_iff]
+  rw [not_iff_comm, not_exists, ← le_principal_iff]
+  simp_rw [← not_le, not_and, not_not]
+  rfl
+
+theorem lt_principal_iff {a : α} {c : DedekindCut α} :
+    c < principal a ↔ ∃ b ∈ c.right, b < a := by
+  rw [← not_le, principal_le_iff]
+  rw [not_iff_comm, not_exists, ← principal_le_iff]
+  rw [← intent_subset_intent_iff]
+  simp_rw [← not_le, not_and, not_not]
+  rfl
+
 end LinearOrder
 end DedekindCut

Mathlib/Topology/Order/Completion.lean

@@ -0,0 +1,127 @@
+/-
+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
+public import Mathlib.Order.UpperLower.CompleteLattice
+public import Mathlib.Order.Completion
+
+import Mathlib.Algebra.Order.Field.Basic
+
+/-!
+# Dense and continuous completion of a linear order
+
+Let `α` be a linear order.
+
+* `DedekindCut.continuous_principal`: the canonical map
+  `DedekindCut.principal : α → DedekindCut α` is continuous for the order topologies.
+* `Order.Fill α`: a dense linear order that extends `α`.
+* `Order.Fill.some`: the order embedding `α ↪o Order.Fill α`/.
+* `Order.Fill.continuous_some`: the map `⇑Order.Fill.some`
+  is continuous for the order topologies.
+* `Order.exists_dense_continuous_completion`:
+  any linear order embeds continuously (for the order topologies)
+  into a dense and complete linear order.
+-/
+
+@[expose] public section
+
+open Set
+
+variable {α : Type*} [LinearOrder α]
+
+theorem DedekindCut.continuous_principal [TopologicalSpace α] [OrderTopology α]
+  [TopologicalSpace (DedekindCut α)] [OrderTopology (DedekindCut α)] :
+    Continuous (fun a : α ↦ principal a) := by
+  rw [OrderTopology.continuous_iff]
+  refine fun c ↦ ⟨?_, ?_⟩
+  · have : IsOpen (⋃ a ∈ c.right, Ioi a) := isOpen_biUnion fun _ _ ↦ isOpen_Ioi
+    convert this
+    ext
+    simp [lt_principal_iff]
+  · have : IsOpen (⋃ a ∈ c.left, Iio a) := isOpen_biUnion fun _ _ ↦ isOpen_Iio
+    convert this
+    ext
+    simp [principal_lt_iff]
+
+namespace Order
+
+/-- 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 (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
+
+universe u
+
+/-- Every linear order embeds continuously in a dense complete linear order. -/
+theorem exists_dense_continuous_completion
+    (α : Type u) [LinearOrder α] [TopologicalSpace α] [OrderTopology α] :
+    ∃ (β : Type u) (_ : CompleteLinearOrder β) (_ : DenselyOrdered β) (_ : TopologicalSpace β)
+      (_ : OrderTopology β) (ι : α ↪o β), Continuous ι :=
+  let : TopologicalSpace (DedekindCut (Fill α)) := Preorder.topology _
+  have : OrderTopology (DedekindCut (Fill α)) := ⟨rfl⟩
+  ⟨_, inferInstance, inferInstance, inferInstance, inferInstance,
+    Fill.some.trans DedekindCut.principalEmbedding,
+    DedekindCut.continuous_principal.comp Fill.continuous_some⟩
+
+end Order

Mathlib/Topology/Sion.lean

@@ -487,9 +487,8 @@ variable [TopologicalSpace F] [AddCommGroup F] [Module ℝ F]
   (hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y : F => f x y) Y)
   (hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y)
 
-/- The following lines essentially assume that `β` has a Dedekind MacNeille completion,
-but this is not in mathlib yet.
-One could then take `ι` to be the embedding of `β` into its DM completion. -/
+/- The following lines essentially assume that `β` has a densely ordered completion.
+(The Dedekind MacNeille completion is not densely ordered unless `β` is.) -/
 variable [TopologicalSpace β] [OrderTopology β]
 variable {γ : Type*} [CompleteLinearOrder γ] [DenselyOrdered γ]
   [TopologicalSpace γ] [OrderTopology γ]