diff --git a/Mathlib.lean b/Mathlib.lean index dfee67d5b36bd4..0eba363413c83f 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Data/Prod/Lex.lean b/Mathlib/Data/Prod/Lex.lean index a51304fbccc323..f43d0585c50a42 100644 --- a/Mathlib/Data/Prod/Lex.lean +++ b/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⟩ diff --git a/Mathlib/Order/Completion.lean b/Mathlib/Order/Completion.lean index 7801e1897790e7..76cda616102183 100644 --- a/Mathlib/Order/Completion.lean +++ 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 diff --git a/Mathlib/Topology/Order/Completion.lean b/Mathlib/Topology/Order/Completion.lean new file mode 100644 index 00000000000000..8aa189003abfef --- /dev/null +++ b/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 diff --git a/Mathlib/Topology/Sion.lean b/Mathlib/Topology/Sion.lean index 0e271efdcdaa49..c533217f496c1a 100644 --- a/Mathlib/Topology/Sion.lean +++ b/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 γ]