From fcb1bfe240dcd4321f3d4b0c674c9d5e5961ff4e Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sat, 11 Apr 2026 22:21:15 +0200 Subject: [PATCH 01/30] initial commit --- Mathlib.lean | 1 + Mathlib/Data/Prod/Lex.lean | 30 ++++++++++++++++++++++++++++ Mathlib/Order/Completion.lean | 37 +++++++++++++++++++++++++++++++++++ 3 files changed, 68 insertions(+) diff --git a/Mathlib.lean b/Mathlib.lean index 6406f1d1165b4d..5fa3ae823f1c02 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5800,6 +5800,7 @@ public import Mathlib.Order.Cover public import Mathlib.Order.Defs.LinearOrder public import Mathlib.Order.Defs.PartialOrder public import Mathlib.Order.Defs.Unbundled +public import Mathlib.Order.DenseCompletion public import Mathlib.Order.DirSupClosed public import Mathlib.Order.Directed public import Mathlib.Order.DirectedInverseSystem diff --git a/Mathlib/Data/Prod/Lex.lean b/Mathlib/Data/Prod/Lex.lean index a51304fbccc323..4817b02b907512 100644 --- a/Mathlib/Data/Prod/Lex.lean +++ b/Mathlib/Data/Prod/Lex.lean @@ -201,6 +201,36 @@ 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] + +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..de506efa3710ed 100644 --- a/Mathlib/Order/Completion.lean +++ b/Mathlib/Order/Completion.lean @@ -105,6 +105,17 @@ 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 (le_of_le_of_eq hy rfl) h⟩ + +lemma le_principal_iff {a : α} {c : DedekindCut α} : + c ≤ principal a ↔ a ∈ c.right := by + simp only [← DedekindCut.upperBounds_left, mem_upperBounds, + ← extent_subset_extent_iff, left_principal] + exact ⟨fun h _ hx ↦ h hx, fun h x hx ↦ h x hx⟩ + /-- 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 +216,36 @@ 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⟩ ↦ lt_of_lt_of_le hca hcb⟩ + rw [← extent_ssubset_extent_iff, Set.ssubset_iff_exists] at h + simp only [← not_le, principal_le_iff] + obtain ⟨c, hcb, hca⟩ := h.2 + refine ⟨c, hca, hcb⟩ + +/-- 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 + simp only [← not_le, le_principal_iff] + exact 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, lt_of_le_of_lt had (by simpa), lt_of_lt_of_le (by simpa) hcb⟩ + end LinearOrder + end DedekindCut From f3a42c74268d09d9c1d90a5cfed34ab4da270fd0 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sat, 11 Apr 2026 22:21:27 +0200 Subject: [PATCH 02/30] add file --- Mathlib/Order/DenseCompletion.lean | 46 ++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 Mathlib/Order/DenseCompletion.lean diff --git a/Mathlib/Order/DenseCompletion.lean b/Mathlib/Order/DenseCompletion.lean new file mode 100644 index 00000000000000..91bbbb344ee3cc --- /dev/null +++ b/Mathlib/Order/DenseCompletion.lean @@ -0,0 +1,46 @@ +/- +Copyright (c) 2026 Antoine Chambert-Loir. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antoine Chambert-Loir +-/ +module + +public import Mathlib.Data.Prod.Lex +public import Mathlib.Order.Completion +public import Mathlib.Order.Hom.WithTopBot + +/-! +# `OrderEmbedding` of a partial order into a dense and complete linear order + +* `DedekindCut.embedLex`: embeds a partial order `α` into `DedekindCut (α ×ₗ β)`. + +* `DedekindCut.embedBotTopLex`: embeds a partial order `α` into `WithBot (WithTop (DedekindCut (α ×ₗ β)))`. + +The interest of these definitions is that when `β` is linearly ordered, densely ordered +and has no extremal elements, the target orders is dense and, +in the second case, complete. It suffices to take `β := ℚ`. + +-/ + +@[expose] public section + +namespace DedekindCut + +open Set Concept + +variable {α β : Type*} [PartialOrder α] [PartialOrder β] + +noncomputable def embedLex (b : β) : + α ↪o DedekindCut (Lex (α × β)) := + RelEmbedding.trans principalEmbedding (factorEmbedding ( + ({toFun c := toLex (c, b), + inj' x y h := by simpa using h, + map_rel_iff' {x y} := by simp [Prod.Lex.toLex_le_toLex, ← le_iff_lt_or_eq] } : α ↪o Lex (α × β)).trans + principalEmbedding)) + +noncomputable def embedBotTopLex (b : β) : + α ↪o WithBot (WithTop (DedekindCut (Lex (α × β)))) := + (RelEmbedding.trans WithTop.coeOrderHom WithBot.coeOrderHom).trans (embedLex b).withTopMap.withBotMap + + +#min_imports From 587f6e4332316943708eb7f7ef9a32d2b4a146d5 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sat, 11 Apr 2026 22:24:06 +0200 Subject: [PATCH 03/30] adjust linter --- Mathlib/Order/DenseCompletion.lean | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/Mathlib/Order/DenseCompletion.lean b/Mathlib/Order/DenseCompletion.lean index 91bbbb344ee3cc..5ab2c09db9951a 100644 --- a/Mathlib/Order/DenseCompletion.lean +++ b/Mathlib/Order/DenseCompletion.lean @@ -12,9 +12,11 @@ public import Mathlib.Order.Hom.WithTopBot /-! # `OrderEmbedding` of a partial order into a dense and complete linear order -* `DedekindCut.embedLex`: embeds a partial order `α` into `DedekindCut (α ×ₗ β)`. +* `DedekindCut.embedLex`: given `b : β`, + embeds a partial order `α` into `DedekindCut (α ×ₗ β)`. -* `DedekindCut.embedBotTopLex`: embeds a partial order `α` into `WithBot (WithTop (DedekindCut (α ×ₗ β)))`. +* `DedekindCut.embedBotTopLex`: given `b : β`, + embeds a partial order `α` into `WithBot (WithTop (DedekindCut (α ×ₗ β)))`. The interest of these definitions is that when `β` is linearly ordered, densely ordered and has no extremal elements, the target orders is dense and, @@ -35,12 +37,13 @@ noncomputable def embedLex (b : β) : RelEmbedding.trans principalEmbedding (factorEmbedding ( ({toFun c := toLex (c, b), inj' x y h := by simpa using h, - map_rel_iff' {x y} := by simp [Prod.Lex.toLex_le_toLex, ← le_iff_lt_or_eq] } : α ↪o Lex (α × β)).trans + map_rel_iff' {x y} := by + simp [Prod.Lex.toLex_le_toLex, ← le_iff_lt_or_eq] } : α ↪o Lex (α × β)).trans principalEmbedding)) noncomputable def embedBotTopLex (b : β) : α ↪o WithBot (WithTop (DedekindCut (Lex (α × β)))) := - (RelEmbedding.trans WithTop.coeOrderHom WithBot.coeOrderHom).trans (embedLex b).withTopMap.withBotMap + (RelEmbedding.trans WithTop.coeOrderHom WithBot.coeOrderHom).trans + (embedLex b).withTopMap.withBotMap - -#min_imports +end DedekindCut From f9caa5a19af875d200700af63a1cf3eecb7228b6 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 12 Apr 2026 00:10:30 +0200 Subject: [PATCH 04/30] attempt --- Mathlib/Order/DenseCompletion.lean | 50 ++++++++++++++++++++++++++++-- Mathlib/Topology/Sion.lean | 49 +++++++++++++++++++++++++++++ 2 files changed, 97 insertions(+), 2 deletions(-) diff --git a/Mathlib/Order/DenseCompletion.lean b/Mathlib/Order/DenseCompletion.lean index 5ab2c09db9951a..a4264b4c12d10e 100644 --- a/Mathlib/Order/DenseCompletion.lean +++ b/Mathlib/Order/DenseCompletion.lean @@ -8,6 +8,7 @@ module public import Mathlib.Data.Prod.Lex public import Mathlib.Order.Completion public import Mathlib.Order.Hom.WithTopBot +public import Mathlib.Topology.Order.Basic /-! # `OrderEmbedding` of a partial order into a dense and complete linear order @@ -30,9 +31,9 @@ namespace DedekindCut open Set Concept -variable {α β : Type*} [PartialOrder α] [PartialOrder β] +variable {α β : Type*} -noncomputable def embedLex (b : β) : +noncomputable def embedLex [PartialOrder α] [PartialOrder β] (b : β) : α ↪o DedekindCut (Lex (α × β)) := RelEmbedding.trans principalEmbedding (factorEmbedding ( ({toFun c := toLex (c, b), @@ -41,9 +42,54 @@ noncomputable def embedLex (b : β) : simp [Prod.Lex.toLex_le_toLex, ← le_iff_lt_or_eq] } : α ↪o Lex (α × β)).trans principalEmbedding)) +variable [LinearOrder α] [TopologicalSpace α] [OrderTopology α] +variable [LinearOrder β] [TopologicalSpace β] [OrderTopology β] + [DenselyOrdered β] [NoMinOrder β] + +#synth DenselyOrdered (DedekindCut (α ×ₗβ)) +#synth CompleteLinearOrder (DedekindCut (α ×ₗβ)) + +example : @OrderTopology (DedekindCut (α ×ₗ β)) (Preorder.topology _) _ := + let := Preorder.topology (DedekindCut (Lex (α × β))) + { topology_eq_generate_intervals := rfl } + +variable [TopologicalSpace (DedekindCut (α ×ₗ β))] + [OrderTopology (DedekindCut (α ×ₗ β))] + +variable {b : β} {ι : α ↪o DedekindCut (α ×ₗ β)} + (hι : ι = embedLex b) + +example : Continuous ι := by + rw [OrderTopology.continuous_iff] + intro c + constructor + · have H (a : α) : a ∈ ι ⁻¹' Ioi c ↔ toLex (a, b) ∉ c.left := by + conv_lhs => + rw [mem_preimage, mem_Ioi] + simp [hι, embedLex] + rw [← not_le, DedekindCut.principal_le_iff] + rw [← DedekindCut.lowerBounds_right] at H + simp only [mem_lowerBounds] at H + push Not at H + rw [isOpen_iff_nhds] + intro a ha + rw [H] at ha + obtain ⟨x, hx⟩ := ha + have : ∃ u v, x = toLex (u, v) := sorry + rcases this with ⟨u, v, rfl⟩ + simp only [Prod.Lex.lt_iff, ofLex_toLex] at hx + intro F hF + simp only [Filter.mem_principal] at hF + rcases hx.2 with (h | h) + · sorry + · sorry + · sorry + +/- noncomputable def embedBotTopLex (b : β) : α ↪o WithBot (WithTop (DedekindCut (Lex (α × β)))) := (RelEmbedding.trans WithTop.coeOrderHom WithBot.coeOrderHom).trans (embedLex b).withTopMap.withBotMap +-/ end DedekindCut diff --git a/Mathlib/Topology/Sion.lean b/Mathlib/Topology/Sion.lean index 52121e51a48a2d..a5ac210dba27a7 100644 --- a/Mathlib/Topology/Sion.lean +++ b/Mathlib/Topology/Sion.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.Convex.Quasiconvex public import Mathlib.Order.SaddlePoint public import Mathlib.Topology.Instances.EReal.Lemmas +public import Mathlib.Order.DenseCompletion /-! # Formalization of Sion's version of the von Neumann minimax theorem @@ -544,4 +545,52 @@ public theorem exists_isSaddlePointOn : end Real +namespace General + +variable {E F β : Type*} [LinearOrder β] +variable {X : Set E} {Y : Set F} {f : E → F → β} +variable [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] + [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] + (ne_X : X.Nonempty) (cX : Convex ℝ X) (kX : IsCompact X) + (hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x : E ↦ f x y) X) + (hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) + +variable [TopologicalSpace F] [AddCommGroup F] [Module ℝ F] + [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] + (cY : Convex ℝ Y) (ne_Y : Y.Nonempty) (kY : IsCompact Y) + (hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y : F => f x y) Y) + (hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) + +variable (β) in +abbrev emb := DedekindCut (β ×ₗ ℚ) + +noncomputable example : CompleteLinearOrder (emb β) := + DedekindCut.instCompleteLinearOrder + +noncomputable example : DenselyOrdered (emb β) := + DedekindCut.instDenselyOrdered + +example : + let _ : TopologicalSpace (emb β) := Preorder.topology (emb β) + OrderTopology (emb β) := by + exact + let x := Preorder.topology (emb β); + { topology_eq_generate_intervals := rfl } + +open DedekindCut + +include ne_X ne_Y cX cY kX kY hfx hfx' hfy hfy' in +/-- The minimax theorem, in the saddle point form -/ +public theorem exists_isSaddlePointOn : + ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b := + let γ := DedekindCut (β ×ₗ ℚ) + let _ : TopologicalSpace β := Preorder.topology β + let _ : TopologicalSpace γ := Preorder.topology γ + have : OrderTopology β := { topology_eq_generate_intervals := rfl } + have : OrderTopology γ := { topology_eq_generate_intervals := rfl } + let ι : β ↪o γ := DedekindCut.embedLex 0 + have hι : Continuous ι := by sorry + DMCompletion.exists_isSaddlePointOn ne_X cX kX hfy hfy' cY ne_Y kY hfx hfx' hι + + end Sion From 6107db0c1ed66796a7f29a164dee8f8593324a6a Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 12 Apr 2026 00:11:54 +0200 Subject: [PATCH 05/30] correct docstring --- Mathlib/Topology/Sion.lean | 53 ++------------------------------------ 1 file changed, 2 insertions(+), 51 deletions(-) diff --git a/Mathlib/Topology/Sion.lean b/Mathlib/Topology/Sion.lean index a5ac210dba27a7..1cd0d2676d66fc 100644 --- a/Mathlib/Topology/Sion.lean +++ b/Mathlib/Topology/Sion.lean @@ -488,9 +488,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.) -/ variable [TopologicalSpace β] [OrderTopology β] variable {γ : Type*} [CompleteLinearOrder γ] [DenselyOrdered γ] [TopologicalSpace γ] [OrderTopology γ] @@ -545,52 +544,4 @@ public theorem exists_isSaddlePointOn : end Real -namespace General - -variable {E F β : Type*} [LinearOrder β] -variable {X : Set E} {Y : Set F} {f : E → F → β} -variable [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] - [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] - (ne_X : X.Nonempty) (cX : Convex ℝ X) (kX : IsCompact X) - (hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x : E ↦ f x y) X) - (hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) - -variable [TopologicalSpace F] [AddCommGroup F] [Module ℝ F] - [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] - (cY : Convex ℝ Y) (ne_Y : Y.Nonempty) (kY : IsCompact Y) - (hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y : F => f x y) Y) - (hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) - -variable (β) in -abbrev emb := DedekindCut (β ×ₗ ℚ) - -noncomputable example : CompleteLinearOrder (emb β) := - DedekindCut.instCompleteLinearOrder - -noncomputable example : DenselyOrdered (emb β) := - DedekindCut.instDenselyOrdered - -example : - let _ : TopologicalSpace (emb β) := Preorder.topology (emb β) - OrderTopology (emb β) := by - exact - let x := Preorder.topology (emb β); - { topology_eq_generate_intervals := rfl } - -open DedekindCut - -include ne_X ne_Y cX cY kX kY hfx hfx' hfy hfy' in -/-- The minimax theorem, in the saddle point form -/ -public theorem exists_isSaddlePointOn : - ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b := - let γ := DedekindCut (β ×ₗ ℚ) - let _ : TopologicalSpace β := Preorder.topology β - let _ : TopologicalSpace γ := Preorder.topology γ - have : OrderTopology β := { topology_eq_generate_intervals := rfl } - have : OrderTopology γ := { topology_eq_generate_intervals := rfl } - let ι : β ↪o γ := DedekindCut.embedLex 0 - have hι : Continuous ι := by sorry - DMCompletion.exists_isSaddlePointOn ne_X cX kX hfy hfy' cY ne_Y kY hfx hfx' hι - - end Sion From 0b89936acf267a9d5e29d4de01549fcc1403bbf9 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 12 Apr 2026 00:13:09 +0200 Subject: [PATCH 06/30] delete DenseCompletion --- Mathlib.lean | 1 - Mathlib/Order/DenseCompletion.lean | 95 ------------------------------ 2 files changed, 96 deletions(-) delete mode 100644 Mathlib/Order/DenseCompletion.lean diff --git a/Mathlib.lean b/Mathlib.lean index 5fa3ae823f1c02..6406f1d1165b4d 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5800,7 +5800,6 @@ public import Mathlib.Order.Cover public import Mathlib.Order.Defs.LinearOrder public import Mathlib.Order.Defs.PartialOrder public import Mathlib.Order.Defs.Unbundled -public import Mathlib.Order.DenseCompletion public import Mathlib.Order.DirSupClosed public import Mathlib.Order.Directed public import Mathlib.Order.DirectedInverseSystem diff --git a/Mathlib/Order/DenseCompletion.lean b/Mathlib/Order/DenseCompletion.lean deleted file mode 100644 index a4264b4c12d10e..00000000000000 --- a/Mathlib/Order/DenseCompletion.lean +++ /dev/null @@ -1,95 +0,0 @@ -/- -Copyright (c) 2026 Antoine Chambert-Loir. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Antoine Chambert-Loir --/ -module - -public import Mathlib.Data.Prod.Lex -public import Mathlib.Order.Completion -public import Mathlib.Order.Hom.WithTopBot -public import Mathlib.Topology.Order.Basic - -/-! -# `OrderEmbedding` of a partial order into a dense and complete linear order - -* `DedekindCut.embedLex`: given `b : β`, - embeds a partial order `α` into `DedekindCut (α ×ₗ β)`. - -* `DedekindCut.embedBotTopLex`: given `b : β`, - embeds a partial order `α` into `WithBot (WithTop (DedekindCut (α ×ₗ β)))`. - -The interest of these definitions is that when `β` is linearly ordered, densely ordered -and has no extremal elements, the target orders is dense and, -in the second case, complete. It suffices to take `β := ℚ`. - --/ - -@[expose] public section - -namespace DedekindCut - -open Set Concept - -variable {α β : Type*} - -noncomputable def embedLex [PartialOrder α] [PartialOrder β] (b : β) : - α ↪o DedekindCut (Lex (α × β)) := - RelEmbedding.trans principalEmbedding (factorEmbedding ( - ({toFun c := toLex (c, b), - inj' x y h := by simpa using h, - map_rel_iff' {x y} := by - simp [Prod.Lex.toLex_le_toLex, ← le_iff_lt_or_eq] } : α ↪o Lex (α × β)).trans - principalEmbedding)) - -variable [LinearOrder α] [TopologicalSpace α] [OrderTopology α] -variable [LinearOrder β] [TopologicalSpace β] [OrderTopology β] - [DenselyOrdered β] [NoMinOrder β] - -#synth DenselyOrdered (DedekindCut (α ×ₗβ)) -#synth CompleteLinearOrder (DedekindCut (α ×ₗβ)) - -example : @OrderTopology (DedekindCut (α ×ₗ β)) (Preorder.topology _) _ := - let := Preorder.topology (DedekindCut (Lex (α × β))) - { topology_eq_generate_intervals := rfl } - -variable [TopologicalSpace (DedekindCut (α ×ₗ β))] - [OrderTopology (DedekindCut (α ×ₗ β))] - -variable {b : β} {ι : α ↪o DedekindCut (α ×ₗ β)} - (hι : ι = embedLex b) - -example : Continuous ι := by - rw [OrderTopology.continuous_iff] - intro c - constructor - · have H (a : α) : a ∈ ι ⁻¹' Ioi c ↔ toLex (a, b) ∉ c.left := by - conv_lhs => - rw [mem_preimage, mem_Ioi] - simp [hι, embedLex] - rw [← not_le, DedekindCut.principal_le_iff] - rw [← DedekindCut.lowerBounds_right] at H - simp only [mem_lowerBounds] at H - push Not at H - rw [isOpen_iff_nhds] - intro a ha - rw [H] at ha - obtain ⟨x, hx⟩ := ha - have : ∃ u v, x = toLex (u, v) := sorry - rcases this with ⟨u, v, rfl⟩ - simp only [Prod.Lex.lt_iff, ofLex_toLex] at hx - intro F hF - simp only [Filter.mem_principal] at hF - rcases hx.2 with (h | h) - · sorry - · sorry - · sorry - -/- -noncomputable def embedBotTopLex (b : β) : - α ↪o WithBot (WithTop (DedekindCut (Lex (α × β)))) := - (RelEmbedding.trans WithTop.coeOrderHom WithBot.coeOrderHom).trans - (embedLex b).withTopMap.withBotMap --/ - -end DedekindCut From 5196de9ba35a7ea5d54b561a3e936ec729f857cf Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 12 Apr 2026 00:13:41 +0200 Subject: [PATCH 07/30] adjust Mathlib after deletion --- Mathlib/Topology/Sion.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Topology/Sion.lean b/Mathlib/Topology/Sion.lean index 1cd0d2676d66fc..a7a699b7d4ec95 100644 --- a/Mathlib/Topology/Sion.lean +++ b/Mathlib/Topology/Sion.lean @@ -8,7 +8,6 @@ module public import Mathlib.Analysis.Convex.Quasiconvex public import Mathlib.Order.SaddlePoint public import Mathlib.Topology.Instances.EReal.Lemmas -public import Mathlib.Order.DenseCompletion /-! # Formalization of Sion's version of the von Neumann minimax theorem From 3312bcd2341b4c96234374d14367bf67ebb90eb4 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 12 Apr 2026 00:45:08 +0200 Subject: [PATCH 08/30] Update Mathlib/Order/Completion.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Violeta Hernández Palacios --- Mathlib/Order/Completion.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Order/Completion.lean b/Mathlib/Order/Completion.lean index de506efa3710ed..5adfb136b3a7d9 100644 --- a/Mathlib/Order/Completion.lean +++ b/Mathlib/Order/Completion.lean @@ -244,7 +244,7 @@ instance [DenselyOrdered α] : DenselyOrdered (DedekindCut α) where 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, lt_of_le_of_lt had (by simpa), lt_of_lt_of_le (by simpa) hcb⟩ + exact ⟨principal u, had.trans_lt (by simpa), hcb.trans_lt' (by simpa)⟩ end LinearOrder From b32d2d49518163665b6e0d6a373e2cdf15ef8370 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 12 Apr 2026 00:45:17 +0200 Subject: [PATCH 09/30] Update Mathlib/Data/Prod/Lex.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Violeta Hernández Palacios --- Mathlib/Data/Prod/Lex.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Data/Prod/Lex.lean b/Mathlib/Data/Prod/Lex.lean index 4817b02b907512..4946376550c3aa 100644 --- a/Mathlib/Data/Prod/Lex.lean +++ b/Mathlib/Data/Prod/Lex.lean @@ -201,6 +201,7 @@ instance [Preorder α] [Preorder β] [DenselyOrdered α] [DenselyOrdered β] : · obtain ⟨c, h₁, h₂⟩ := exists_between h exact ⟨(a, c), right _ h₁, right _ h₂⟩ +@[to_dual] instance [Preorder α] [Preorder β] [NoMinOrder β] [DenselyOrdered β] : DenselyOrdered (α ×ₗ β) where dense x y h := by From 95b570afb450506d7a82296d7d63b97708f5ce78 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 12 Apr 2026 00:45:57 +0200 Subject: [PATCH 10/30] Update Mathlib/Order/Completion.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Violeta Hernández Palacios --- Mathlib/Order/Completion.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/Order/Completion.lean b/Mathlib/Order/Completion.lean index 5adfb136b3a7d9..0be13b4315a9c0 100644 --- a/Mathlib/Order/Completion.lean +++ b/Mathlib/Order/Completion.lean @@ -112,9 +112,8 @@ lemma principal_le_iff {a : α} {c : DedekindCut α} : lemma le_principal_iff {a : α} {c : DedekindCut α} : c ≤ principal a ↔ a ∈ c.right := by - simp only [← DedekindCut.upperBounds_left, mem_upperBounds, - ← extent_subset_extent_iff, left_principal] - exact ⟨fun h _ hx ↦ h hx, fun h x hx ↦ h x hx⟩ + 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 α) := From 8692fb912de42051ecc2fd61367146655ba60aee Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 12 Apr 2026 00:46:11 +0200 Subject: [PATCH 11/30] Update Mathlib/Order/Completion.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Violeta Hernández Palacios --- Mathlib/Order/Completion.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Order/Completion.lean b/Mathlib/Order/Completion.lean index 0be13b4315a9c0..1b446f4b3dbb62 100644 --- a/Mathlib/Order/Completion.lean +++ b/Mathlib/Order/Completion.lean @@ -108,7 +108,7 @@ theorem principal_lt_principal {a b : α} : principal a < principal b ↔ a < b 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 (le_of_le_of_eq hy rfl) h⟩ + 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 From 282b045b78b27c27e695b9be5f905f5cbe4ed382 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 12 Apr 2026 00:46:20 +0200 Subject: [PATCH 12/30] Update Mathlib/Order/Completion.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Violeta Hernández Palacios --- Mathlib/Order/Completion.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Order/Completion.lean b/Mathlib/Order/Completion.lean index 1b446f4b3dbb62..9c4b665ae6179b 100644 --- a/Mathlib/Order/Completion.lean +++ b/Mathlib/Order/Completion.lean @@ -218,7 +218,7 @@ noncomputable instance : LinearOrder (DedekindCut α) where /-- 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⟩ ↦ lt_of_lt_of_le hca hcb⟩ + refine ⟨fun h ↦ ?_, fun ⟨c, hca, hcb⟩ ↦ hca.trans_le hcb⟩ rw [← extent_ssubset_extent_iff, Set.ssubset_iff_exists] at h simp only [← not_le, principal_le_iff] obtain ⟨c, hcb, hca⟩ := h.2 From c981710878cd0051e34926982cd07e15de6b1731 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 12 Apr 2026 00:46:28 +0200 Subject: [PATCH 13/30] Update Mathlib/Order/Completion.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Violeta Hernández Palacios --- Mathlib/Order/Completion.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Mathlib/Order/Completion.lean b/Mathlib/Order/Completion.lean index 9c4b665ae6179b..c8d6057b67ce26 100644 --- a/Mathlib/Order/Completion.lean +++ b/Mathlib/Order/Completion.lean @@ -220,9 +220,7 @@ 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 - simp only [← not_le, principal_le_iff] - obtain ⟨c, hcb, hca⟩ := h.2 - refine ⟨c, hca, hcb⟩ + 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 α} : From aac653852f7c7b2a7b5f2c6025864c7bd6e5ff6c Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 12 Apr 2026 00:46:36 +0200 Subject: [PATCH 14/30] Update Mathlib/Order/Completion.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Violeta Hernández Palacios --- Mathlib/Order/Completion.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Order/Completion.lean b/Mathlib/Order/Completion.lean index c8d6057b67ce26..8997be27f70cc8 100644 --- a/Mathlib/Order/Completion.lean +++ b/Mathlib/Order/Completion.lean @@ -227,8 +227,7 @@ 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 - simp only [← not_le, le_principal_iff] - exact h.2 + simpa [← not_le, le_principal_iff] using h.2 noncomputable instance : CompleteLinearOrder (DedekindCut α) where __ := (inferInstance : LinearOrder _) From b8059945601aa8cc7c69bf81b436b7fff52dc788 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 12 Apr 2026 00:46:49 +0200 Subject: [PATCH 15/30] Update Mathlib/Order/Completion.lean MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Violeta Hernández Palacios --- Mathlib/Order/Completion.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Order/Completion.lean b/Mathlib/Order/Completion.lean index 8997be27f70cc8..bbafd82776e8fc 100644 --- a/Mathlib/Order/Completion.lean +++ b/Mathlib/Order/Completion.lean @@ -243,5 +243,4 @@ instance [DenselyOrdered α] : DenselyOrdered (DedekindCut α) where exact ⟨principal u, had.trans_lt (by simpa), hcb.trans_lt' (by simpa)⟩ end LinearOrder - end DedekindCut From 80d17ddc241deb34c9d830ec1d7de0a503d2df07 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 12 Apr 2026 10:22:45 +0200 Subject: [PATCH 16/30] modify to_dual tag --- Mathlib/Data/Prod/Lex.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Prod/Lex.lean b/Mathlib/Data/Prod/Lex.lean index 4946376550c3aa..f43d0585c50a42 100644 --- a/Mathlib/Data/Prod/Lex.lean +++ b/Mathlib/Data/Prod/Lex.lean @@ -201,7 +201,6 @@ instance [Preorder α] [Preorder β] [DenselyOrdered α] [DenselyOrdered β] : · obtain ⟨c, h₁, h₂⟩ := exists_between h exact ⟨(a, c), right _ h₁, right _ h₂⟩ -@[to_dual] instance [Preorder α] [Preorder β] [NoMinOrder β] [DenselyOrdered β] : DenselyOrdered (α ×ₗ β) where dense x y h := by @@ -217,6 +216,7 @@ instance [Preorder α] [Preorder β] [NoMinOrder β] [DenselyOrdered β] : 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 From e2d9c938332c7e11e97f2ec19030b1711d1602c8 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Wed, 15 Apr 2026 14:15:37 +0200 Subject: [PATCH 17/30] add Fill file --- Mathlib.lean | 1 + Mathlib/Order/Completion.lean | 43 ++- Mathlib/Order/Fill.lean | 493 ++++++++++++++++++++++++++++++++++ 3 files changed, 535 insertions(+), 2 deletions(-) create mode 100644 Mathlib/Order/Fill.lean diff --git a/Mathlib.lean b/Mathlib.lean index 6406f1d1165b4d..ac3ef8a56346e4 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5807,6 +5807,7 @@ public import Mathlib.Order.Disjoint public import Mathlib.Order.Disjointed public import Mathlib.Order.Extension.Linear public import Mathlib.Order.Extension.Well +public import Mathlib.Order.Fill public import Mathlib.Order.Filter.AtTopBot.Archimedean public import Mathlib.Order.Filter.AtTopBot.Basic public import Mathlib.Order.Filter.AtTopBot.BigOperators diff --git a/Mathlib/Order/Completion.lean b/Mathlib/Order/Completion.lean index bbafd82776e8fc..e6ddf63eb6cdc4 100644 --- a/Mathlib/Order/Completion.lean +++ b/Mathlib/Order/Completion.lean @@ -7,8 +7,8 @@ module public import Mathlib.Order.Concept -import Mathlib.Order.UpperLower.CompleteLattice - +public import Mathlib.Order.UpperLower.CompleteLattice +public import Mathlib.Topology.Order.Basic /-! # Dedekind-MacNeille completion @@ -242,5 +242,44 @@ instance [DenselyOrdered α] : DenselyOrdered (DedekindCut α) where 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 + +theorem continuous_principal [TopologicalSpace α] [OrderTopology α] + [TopologicalSpace (DedekindCut α)] [OrderTopology (DedekindCut α)] : + Continuous (fun a : α ↦ principal a) := by + rw [OrderTopology.continuous_iff] + intro c + simp only [isOpen_iff_nhds] + refine ⟨fun a ↦ ?_, fun a ↦ ?_⟩ + · simp only [mem_preimage, mem_Ioi, Filter.le_principal_iff] + rw [lt_principal_iff] + rintro ⟨b, hb, hba⟩ + rw [mem_nhds_iff] + use Ioi b + refine ⟨fun x ↦ ?_, isOpen_Ioi, mem_Ioi.mpr hba⟩ + simp only [mem_Ioi, mem_preimage, lt_principal_iff] + exact fun h ↦ ⟨b, ⟨hb, h⟩⟩ + · simp only [mem_preimage, mem_Iio, Filter.le_principal_iff] + rw [principal_lt_iff] + rintro ⟨b, hb, hba⟩ + rw [mem_nhds_iff] + use Iio b + refine ⟨fun x ↦ ?_, isOpen_Iio, mem_Iio.mpr hba⟩ + simp only [mem_Iio, mem_preimage, principal_lt_iff] + refine fun h ↦ ⟨b, ⟨hb, h⟩⟩ + end LinearOrder end DedekindCut diff --git a/Mathlib/Order/Fill.lean b/Mathlib/Order/Fill.lean new file mode 100644 index 00000000000000..f6e293e730d405 --- /dev/null +++ b/Mathlib/Order/Fill.lean @@ -0,0 +1,493 @@ +/- +Copyright (c) 2026 Antoine Chambert-Loir. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Antoine Chambert-Loir +-/ +module + +public import Mathlib.Data.Prod.Lex +public import Mathlib.Order.Completion +public import Mathlib.Order.Hom.WithTopBot +public import Mathlib.Topology.Order.Basic + +/-! +# `OrderEmbedding` of a partial order into a dense and complete linear order + +* `DedekindCut.embedLex`: given `b : β`, + embeds a partial order `α` into `DedekindCut (α ×ₗ β)`. + +* `DedekindCut.embedBotTopLex`: given `b : β`, + embeds a partial order `α` into `WithBot (WithTop (DedekindCut (α ×ₗ β)))`. + +The interest of these definitions is that when `β` is linearly ordered, densely ordered +and has no extremal elements, the target orders is dense and, +in the second case, complete. It suffices to take `β := ℚ`. + +-/ + +@[expose] public section + +namespace Order + +/-- a `Hole` in a partial order is a (nontrivially) empty open interval -/ +structure Hole (α : Type*) [PartialOrder α] where + left : α + right : α + left_lt_right : left < right + Ioo_empty : Set.Ioo left right = ∅ + +namespace Hole + +section PartialOrder + +variable {α : Type*} [PartialOrder α] + +theorem forall_notMem (x : Hole α) (a : α) : ¬ a ∈ Set.Ioo x.left x.right := + Set.eq_empty_iff_forall_notMem.mp x.Ioo_empty a + +/- This is not the good definition for a preorder, +because one should identify holes ]a;b[ and ]c;d[ when a ~ c and b ~ d ! -/ + +/-- The natural preordering on `Hole α` -/ +instance : Preorder (Hole α) where + le x y := x.left ≤ y.left + lt x y := x.left < y.left + le_refl _ := by simp + le_trans x y z h k := Preorder.le_trans _ _ _ h k + lt_iff_le_not_ge x y := Preorder.lt_iff_le_not_ge x.left y.left + +theorem lt_iff_left {x y : Hole α} : x < y ↔ x.left < y.left := Iff.rfl + +theorem le_iff_left {x y : Hole α} : x ≤ y ↔ x.left ≤ y.left := Iff.rfl + +end PartialOrder + +section LinearOrder + +variable {α : Type*} [LinearOrder α] + +theorem le_right_of_lt_left (x : Hole α) (a : α) (h : x.left < a) : x.right ≤ a := by + rw [← not_lt] + intro k + apply x.forall_notMem a ⟨h, k⟩ + +theorem le_left_of_lt_right (x : Hole α) (a : α) (h : a < x.right) : a ≤ x.left := by + rw [← not_lt] + intro k + apply x.forall_notMem a ⟨k, h⟩ + +theorem lt_iff_right {x y : Hole α} : x < y ↔ x.right < y.right := by + rw [Hole.lt_iff_left] + constructor + · intro hl + rw [← not_le] + exact fun hr ↦ x.forall_notMem y.left ⟨hl, lt_of_lt_of_le y.left_lt_right hr⟩ + · intro hr + rw [← not_le] + exact fun hl ↦ y.forall_notMem x.right ⟨lt_of_le_of_lt hl x.left_lt_right, hr⟩ + +theorem le_iff_right {x y : Hole α} : x ≤ y ↔ x.right ≤ y.right := by + simpa [Hole.le_iff_left, ← not_lt, not_iff_not] using lt_iff_right + +/-- The natural partial ordering on `Hole α` -/ +instance : PartialOrder (Hole α) where + le_antisymm x y h k := by + rw [mk.injEq] + exact ⟨le_antisymm (le_iff_left.mpr h) (le_iff_left.mpr k), + le_antisymm (le_iff_right.mp h) (le_iff_right.mp k)⟩ + +theorem left_injective : Function.Injective (fun x : Hole α ↦ x.left) := fun x y h ↦ by + rw [mk.injEq] + refine ⟨h, ?_⟩ + simp [le_antisymm_iff, ← le_iff_right, le_iff_left, h] + +theorem right_injective : Function.Injective (fun x : Hole α ↦ x.right) := fun x y h ↦ by + rw [mk.injEq] + refine ⟨?_, h⟩ + simp [le_antisymm_iff, ← le_iff_left, le_iff_right, h] + +noncomputable instance : LinearOrder (Hole α) where + le_total x t := by simp [le_iff_left, Std.le_total] + toDecidableLE := Classical.decRel LE.le + +end LinearOrder + +end Hole + +/-- The `Fill α f` of a preorder `α` replaces all `x : Hole α` with the preorder `f x` -/ +inductive Fill {α : Type*} [PartialOrder α] (f : Hole α → Type*) + | some (a : α) + | hole (x : Hole α) (t : f x) + +namespace Fill + +section lt + +variable {α : Type*} [PartialOrder α] (f : Hole α → Type*) [∀ x, LT (f x)] + +instance : LT (Fill f) where + lt + | some (a : α), some (b : α) => a < b + | some (a : α), hole y _ => a ≤ y.left + | hole x _, some b => x.right ≤ b + | hole x t, hole y u => x < y ∨ ∃ (h : y = x), t < h ▸ u + +variable {f} + +theorem some_lt_some_iff {a b : α} : (some a : Fill f) < some b ↔ a < b := Iff.rfl + +theorem some_lt_hole_iff {a : α} {y : Hole α} {u : f y} : + some a < hole y u ↔ a ≤ y.left:= Iff.rfl + +theorem hole_lt_some_iff {x : Hole α} {t : f x} {b : α} : + hole x t < some b ↔ x.right ≤ b := Iff.rfl + +theorem hole_lt_hole_iff {x y : Hole α} {t : f x} {u : f y} : + hole x t < hole y u ↔ x < y ∨ ∃ (h : y = x), t < h ▸ u := + Iff.rfl + +theorem hole_lt_hole_of_left {x y : Hole α} {t : f x} {u : f y} + (h : x < y) : hole x t < hole y u := by + simp [hole_lt_hole_iff, h] + +theorem hole_lt_hole_of_right {x : Hole α} {t u : f x} (h : t < u) : hole x t < hole x u := by + simp [hole_lt_hole_iff, h] + +end lt + +section le + +variable {α : Type*} [PartialOrder α] (f : Hole α → Type*) [∀ x, LE (f x)] + +instance : LE (Fill f) where + le + | some (a : α), some (b : α) => a ≤ b + | some (a : α), hole y _ => a ≤ y.left + | hole y _, some b => y.right ≤ b + | hole x t, hole y u => x < y ∨ ∃ (h : y = x), t ≤ h ▸ u + +theorem some_le_some_iff {a b : α} : (some a : Fill f) ≤ some b ↔ a ≤ b := Iff.rfl + +theorem some_le_hole_iff {a : α} {y : Hole α} {u : f y} : + some a ≤ hole y u ↔ a ≤ y.left:= Iff.rfl + +theorem hole_le_some_iff {x : Hole α} {t : f x} {b : α} : + hole x t ≤ some b ↔ x.right ≤ b := Iff.rfl + +theorem hole_le_hole_iff {x y : Hole α} {t : f x} {u : f y} : + hole x t ≤ hole y u ↔ x < y ∨ ∃ (h : y = x), t ≤ h ▸ u := + Iff.rfl + +theorem hole_le_hole_of_left {x y : Hole α} {t : f x} {u : f y} + (h : x < y) : hole x t ≤ hole y u := by + simp [hole_le_hole_iff, h] + +theorem hole_le_hole_iff_right {x : Hole α} {t u : f x} : + hole x t ≤ hole x u ↔ t ≤ u := by + simp [hole_le_hole_iff] + +theorem hole_le_hole_of_right {x : Hole α} {t u : f x} (h : t ≤ u) : hole x t ≤ hole x u := by + simp [hole_le_hole_iff, h] + +end le + +section partialorder + +variable {α : Type*} [PartialOrder α] {f : Hole α → Type*} [∀ x, PartialOrder (f x)] + +theorem hole_lt_hole_iff_right {x : Hole α} {t u : f x} : + hole x t < hole x u ↔ t < u := by + simp only [hole_lt_hole_iff, exists_const, or_iff_right_iff_imp, lt_irrefl x] + exact False.elim + +end partialorder + +section linear + +variable {α : Type*} [LinearOrder α] {f : Hole α → Type*} + +instance [∀ x, PartialOrder (f x)] : PartialOrder (Fill f) where + le_refl x := match x with + | some a => by simp [some_le_some_iff] + | hole x t => by simp [hole_le_hole_iff] + le_trans x y z := match x, y, z with + | some a, some b, some c => by + simp only [some_le_some_iff] + exact le_trans + | some a, hole y u, some c => by + simp only [some_le_hole_iff, hole_le_some_iff, some_le_some_iff] + intro h k + exact le_trans h (le_trans y.left_lt_right.le k) + | hole x t, some b, some c => by + simp only [hole_le_some_iff, some_le_some_iff] + exact le_trans + | hole x t, hole y u, some c => by + simp only [hole_le_hole_iff, hole_le_some_iff] + rintro (h | ⟨e, h⟩) k + · apply le_trans _ k + simp [← x.le_iff_right, h.le] + · simp [← e, k] + | some a, some b, hole z v => by + simp only [some_le_some_iff, some_le_hole_iff] + exact le_trans + | some a, hole y u, hole z v => by + simp only [some_le_hole_iff, hole_le_hole_iff] + rintro h (k | ⟨e, k⟩) + · apply le_trans h + rw [← Hole.le_iff_left] + exact k.le + · simp [e, h] + | hole x t, some b, hole z v => by + rw [hole_le_some_iff, some_le_hole_iff, hole_le_hole_iff] + intro h k + apply Or.intro_left + rw [Hole.lt_iff_left] + exact lt_of_lt_of_le x.left_lt_right (le_trans h k) + | hole x t, hole y u, hole z v => by + simp only [hole_le_hole_iff] + rintro (h | ⟨e, h⟩) (k | ⟨e', k⟩) + · left; exact lt_trans h k + · left; rwa [e'] + · left; rwa [← e] + · right + subst e' e + simp only [exists_const] at h k ⊢ + exact le_trans h k + le_antisymm x y h k := by + match x, y with + | some a, some b => + simp only [some_le_some_iff] at h k + simp only [some.injEq] + exact le_antisymm h k + | some a, hole y u => + apply False.elim + simp only [some_le_hole_iff] at h + simp only [hole_le_some_iff] at k + exact lt_irrefl a <| lt_of_le_of_lt h (lt_of_lt_of_le y.left_lt_right k) + | hole x t, some b => + apply False.elim + simp only [hole_le_some_iff] at h + simp only [some_le_hole_iff] at k + exact lt_irrefl b <| lt_of_le_of_lt k (lt_of_lt_of_le x.left_lt_right h) + | hole x t, hole y u => + rw [hole_le_hole_iff] at h k + rcases h with (h | ⟨e, h⟩) + · apply False.elim + apply lt_irrefl x + rcases k with (k | ⟨e', k⟩) + · exact lt_trans h k + · exact lt_of_lt_of_eq h e'.symm + · subst e + simp only at h + simp only [lt_self_iff_false, exists_const, false_or] at k + rw [le_antisymm h k] + lt_iff_le_not_ge x y := match x, y with + | some a, some b => by + simp only [some_lt_some_iff, some_le_some_iff] + exact lt_iff_le_not_ge + | some a, hole y u => by + rw [some_lt_hole_iff, some_le_hole_iff, hole_le_some_iff] + simp only [iff_self_and] + intro h k + exact lt_irrefl a (lt_of_le_of_lt h (lt_of_lt_of_le y.left_lt_right k)) + | hole x t, some b => by + rw [some_le_hole_iff, hole_le_some_iff, hole_lt_some_iff] + simp only [iff_self_and] + intro h k + exact lt_irrefl b (lt_of_le_of_lt k (lt_of_lt_of_le x.left_lt_right h)) + | hole x t, hole y u => by + simp only [hole_lt_hole_iff, hole_le_hole_iff] + rw [not_or, not_exists] + constructor + · rintro (h | ⟨e, h⟩) + · refine ⟨Or.intro_left _ h, Std.not_gt_of_lt h, + fun e k ↦ lt_irrefl x (lt_of_lt_of_eq h e.symm)⟩ + · refine ⟨Or.intro_right _ ⟨e, h.le⟩, e.symm.not_gt, fun _ ↦ ?_⟩ + subst e + simp only at h ⊢ + exact Std.not_le_of_gt h + · rintro ⟨(h | ⟨e, h⟩), k, k'⟩ + · apply Or.intro_left _ h + · apply Or.intro_right + subst e + simp only [lt_iff_le_not_ge, exists_const] + exact ⟨h, k' rfl⟩ + +variable [∀ x, LinearOrder (f x)] + +/-- The linear ordering on `Fill f` when `a` and all `f x` are linearly ordered -/ +noncomputable instance : LinearOrder (Fill f) where + toDecidableLE := Classical.decRel LE.le + le_total x y := match x, y with + | some a, some b => by simp only [some_le_some_iff, le_total] + | some a, hole y u => by + simp only [some_le_hole_iff, hole_le_some_iff] + apply Or.imp (h := le_or_gt a y.left) id + exact y.le_right_of_lt_left a + | hole x t, some b => by + simp only [some_le_hole_iff, hole_le_some_iff] + apply Or.imp (h := le_or_gt x.right b) id + exact Hole.le_left_of_lt_right x b + | hole x t, hole y u => by + simp only [hole_le_hole_iff] + rcases lt_trichotomy x y with (h | h | h) + · left; left; exact h + · subst h + simp [le_total] + · right; left; exact h + +instance [∀ x, Nonempty (f x)] [∀ x, NoMinOrder (f x)] [∀ x, NoMaxOrder (f x)] + [∀ x, DenselyOrdered (f x)] : DenselyOrdered (Fill f) where + dense x y h := match x, y with + | some a, some b => by + simp only [some_lt_some_iff] at h + rcases (Set.Ioo a b).eq_empty_or_nonempty with (k | ⟨⟨c, k⟩⟩) + · let x : Hole α := ⟨a, b, h, k⟩ + let t : f x := Classical.ofNonempty + refine ⟨hole x t, by simp [some_lt_hole_iff, hole_lt_some_iff, x]⟩ + · use some c + simp [some_lt_some_iff] + exact k + | some a, hole y u => by + obtain ⟨t, ht⟩ := exists_lt u + use hole y t + simp only [some_lt_hole_iff, hole_lt_hole_iff] at h ⊢ + simp [h, ht] + | hole x t, some b => by + obtain ⟨u, hu⟩ := exists_gt t + use hole x u + simp only [hole_lt_hole_iff, hole_lt_some_iff] at h ⊢ + simp [hu, h] + | hole x t, hole y u => by + simp only [hole_lt_hole_iff] at h + rcases h with (h | ⟨e, h⟩) + · obtain ⟨v, hv⟩ := exists_gt t + use hole x v + simp [hole_lt_hole_iff, h, hv] + · subst e + simp only at h + obtain ⟨v, hv, hv'⟩ := DenselyOrdered.dense t u h + use hole y v + simp [hole_lt_hole_iff, hv, hv'] + +theorem continuous_some [TopologicalSpace α] [OrderTopology α] + [∀ x, Nonempty (f x)] [∀ x, NoMinOrder (f x)] [∀ x, NoMaxOrder (f x)] + [∀ x, DenselyOrdered (f x)] + [TopologicalSpace (Fill f)] [OrderTopology (Fill f)] : + Continuous (fun a ↦ (some a : Fill f)) := by + rw [OrderTopology.continuous_iff] + intro x + simp only [isOpen_iff_nhds] + match x with + | some a => + refine ⟨fun b h ↦ ?_, fun b h ↦ ?_⟩ + · simp only [Set.mem_preimage, Set.mem_Ioi, some_lt_some_iff] at h + simp only [Filter.le_principal_iff, mem_nhds_iff] + rcases (Set.Ioo a b).eq_empty_or_nonempty with (k | ⟨⟨c, k⟩⟩) + · let x : Hole α := ⟨a, b, h, k⟩ + let t : f x := Classical.ofNonempty + refine ⟨Set.Ioi a, fun c h ↦ ?_, isOpen_Ioi, h⟩ + simp only [Set.mem_preimage, Set.mem_Ioi, some_lt_some_iff] + exact h + · refine ⟨Set.Ioi c, fun x h ↦ ?_, isOpen_Ioi, k.2⟩ + simp only [Set.mem_preimage, Set.mem_Ioi, some_lt_some_iff] + apply lt_trans k.1 h + · simp only [Set.mem_preimage, Set.mem_Iio, some_lt_some_iff] at h + simp only [Filter.le_principal_iff, mem_nhds_iff] + rcases (Set.Ioo b a).eq_empty_or_nonempty with (k | ⟨⟨c, k⟩⟩) + · let x : Hole α := ⟨b, a, h, k⟩ + let t : f x := Classical.ofNonempty + refine ⟨Set.Iio a, fun c h ↦ ?_, isOpen_Iio, h⟩ + simp only [Set.mem_preimage, Set.mem_Iio, some_lt_some_iff] + exact h + · refine ⟨Set.Iio c, fun x h ↦ ?_, isOpen_Iio, k.1⟩ + simp only [Set.mem_preimage, Set.mem_Iio, some_lt_some_iff] + apply lt_trans h k.2 + | hole x t => + refine ⟨fun a h ↦ ?_, fun a h ↦ ?_⟩ + · simp only [Set.mem_preimage, Set.mem_Ioi, hole_lt_some_iff] at h + rw [Filter.le_principal_iff, mem_nhds_iff] + refine ⟨Set.Ioi x.left, fun b k ↦ ?_, isOpen_Ioi, lt_of_lt_of_le x.left_lt_right h⟩ + simp only [Set.mem_preimage, Set.mem_Ioi, hole_lt_some_iff] + exact Hole.le_right_of_lt_left x b k + · simp only [Set.mem_preimage, Set.mem_Iio, some_lt_hole_iff] at h + rw [Filter.le_principal_iff, mem_nhds_iff] + refine ⟨Set.Iio x.right, fun b k ↦ ?_, isOpen_Iio, ?_⟩ + · simp only [Set.mem_preimage, Set.mem_Iio, some_lt_hole_iff] + exact Hole.le_left_of_lt_right x b k + · apply lt_of_le_of_lt h x.left_lt_right + +end linear + +end Fill + +end Order + +end + +/- +namespace DedekindCut + +open Set Concept + +noncomputable def embedLex [PartialOrder α] [PartialOrder β] (b : β) : + α ↪o DedekindCut (Lex (α × β)) := + RelEmbedding.trans principalEmbedding (factorEmbedding ( + ({toFun c := toLex (c, b), + inj' x y h := by simpa using h, + map_rel_iff' {x y} := by + simp [Prod.Lex.toLex_le_toLex, ← le_iff_lt_or_eq] } : α ↪o Lex (α × β)).trans + principalEmbedding)) + +variable [LinearOrder α] [TopologicalSpace α] [OrderTopology α] +variable [LinearOrder β] [TopologicalSpace β] [OrderTopology β] + [DenselyOrdered β] [NoMinOrder β] + +#synth DenselyOrdered (DedekindCut (α ×ₗβ)) +#synth CompleteLinearOrder (DedekindCut (α ×ₗβ)) + +example : @OrderTopology (DedekindCut (α ×ₗ β)) (Preorder.topology _) _ := + let := Preorder.topology (DedekindCut (Lex (α × β))) + { topology_eq_generate_intervals := rfl } + +variable [TopologicalSpace (DedekindCut (α ×ₗ β))] + [OrderTopology (DedekindCut (α ×ₗ β))] + +variable {b : β} {ι : α ↪o DedekindCut (α ×ₗ β)} + (hι : ι = embedLex b) + +example : Continuous ι := by + rw [OrderTopology.continuous_iff] + intro c + constructor + · have H (a : α) : a ∈ ι ⁻¹' Ioi c ↔ toLex (a, b) ∉ c.left := by + conv_lhs => + rw [mem_preimage, mem_Ioi] + simp [hι, embedLex] + rw [← not_le, DedekindCut.principal_le_iff] + rw [← DedekindCut.lowerBounds_right] at H + simp only [mem_lowerBounds] at H + push Not at H + rw [isOpen_iff_nhds] + intro a ha + rw [H] at ha + obtain ⟨x, hx⟩ := ha + have : ∃ u v, x = toLex (u, v) := sorry + rcases this with ⟨u, v, rfl⟩ + simp only [Prod.Lex.lt_iff, ofLex_toLex] at hx + intro F hF + simp only [Filter.mem_principal] at hF + rcases hx.2 with (h | h) + · sorry + · sorry + · sorry + +/- +noncomputable def embedBotTopLex (b : β) : + α ↪o WithBot (WithTop (DedekindCut (Lex (α × β)))) := + (RelEmbedding.trans WithTop.coeOrderHom WithBot.coeOrderHom).trans + (embedLex b).withTopMap.withBotMap +-/ + +end DedekindCut +-/ From 3f200df725f1fadf4d5bd68109d6f40676f1b3e4 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Fri, 17 Apr 2026 22:00:59 +0200 Subject: [PATCH 18/30] use code by VHP --- Mathlib.lean | 2 +- Mathlib/Order/Completion.lean | 27 +- Mathlib/Order/Fill.lean | 493 ---------------------------------- 3 files changed, 2 insertions(+), 520 deletions(-) delete mode 100644 Mathlib/Order/Fill.lean diff --git a/Mathlib.lean b/Mathlib.lean index ac3ef8a56346e4..cfc1e99d163c97 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5807,7 +5807,6 @@ public import Mathlib.Order.Disjoint public import Mathlib.Order.Disjointed public import Mathlib.Order.Extension.Linear public import Mathlib.Order.Extension.Well -public import Mathlib.Order.Fill public import Mathlib.Order.Filter.AtTopBot.Archimedean public import Mathlib.Order.Filter.AtTopBot.Basic public import Mathlib.Order.Filter.AtTopBot.BigOperators @@ -7736,6 +7735,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/Order/Completion.lean b/Mathlib/Order/Completion.lean index e6ddf63eb6cdc4..c4a80b8921424f 100644 --- a/Mathlib/Order/Completion.lean +++ b/Mathlib/Order/Completion.lean @@ -6,9 +6,8 @@ Authors: Violeta Hernández Palacios module public import Mathlib.Order.Concept - public import Mathlib.Order.UpperLower.CompleteLattice -public import Mathlib.Topology.Order.Basic + /-! # Dedekind-MacNeille completion @@ -257,29 +256,5 @@ theorem lt_principal_iff {a : α} {c : DedekindCut α} : simp_rw [← not_le, not_and, not_not] rfl -theorem continuous_principal [TopologicalSpace α] [OrderTopology α] - [TopologicalSpace (DedekindCut α)] [OrderTopology (DedekindCut α)] : - Continuous (fun a : α ↦ principal a) := by - rw [OrderTopology.continuous_iff] - intro c - simp only [isOpen_iff_nhds] - refine ⟨fun a ↦ ?_, fun a ↦ ?_⟩ - · simp only [mem_preimage, mem_Ioi, Filter.le_principal_iff] - rw [lt_principal_iff] - rintro ⟨b, hb, hba⟩ - rw [mem_nhds_iff] - use Ioi b - refine ⟨fun x ↦ ?_, isOpen_Ioi, mem_Ioi.mpr hba⟩ - simp only [mem_Ioi, mem_preimage, lt_principal_iff] - exact fun h ↦ ⟨b, ⟨hb, h⟩⟩ - · simp only [mem_preimage, mem_Iio, Filter.le_principal_iff] - rw [principal_lt_iff] - rintro ⟨b, hb, hba⟩ - rw [mem_nhds_iff] - use Iio b - refine ⟨fun x ↦ ?_, isOpen_Iio, mem_Iio.mpr hba⟩ - simp only [mem_Iio, mem_preimage, principal_lt_iff] - refine fun h ↦ ⟨b, ⟨hb, h⟩⟩ - end LinearOrder end DedekindCut diff --git a/Mathlib/Order/Fill.lean b/Mathlib/Order/Fill.lean deleted file mode 100644 index f6e293e730d405..00000000000000 --- a/Mathlib/Order/Fill.lean +++ /dev/null @@ -1,493 +0,0 @@ -/- -Copyright (c) 2026 Antoine Chambert-Loir. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Antoine Chambert-Loir --/ -module - -public import Mathlib.Data.Prod.Lex -public import Mathlib.Order.Completion -public import Mathlib.Order.Hom.WithTopBot -public import Mathlib.Topology.Order.Basic - -/-! -# `OrderEmbedding` of a partial order into a dense and complete linear order - -* `DedekindCut.embedLex`: given `b : β`, - embeds a partial order `α` into `DedekindCut (α ×ₗ β)`. - -* `DedekindCut.embedBotTopLex`: given `b : β`, - embeds a partial order `α` into `WithBot (WithTop (DedekindCut (α ×ₗ β)))`. - -The interest of these definitions is that when `β` is linearly ordered, densely ordered -and has no extremal elements, the target orders is dense and, -in the second case, complete. It suffices to take `β := ℚ`. - --/ - -@[expose] public section - -namespace Order - -/-- a `Hole` in a partial order is a (nontrivially) empty open interval -/ -structure Hole (α : Type*) [PartialOrder α] where - left : α - right : α - left_lt_right : left < right - Ioo_empty : Set.Ioo left right = ∅ - -namespace Hole - -section PartialOrder - -variable {α : Type*} [PartialOrder α] - -theorem forall_notMem (x : Hole α) (a : α) : ¬ a ∈ Set.Ioo x.left x.right := - Set.eq_empty_iff_forall_notMem.mp x.Ioo_empty a - -/- This is not the good definition for a preorder, -because one should identify holes ]a;b[ and ]c;d[ when a ~ c and b ~ d ! -/ - -/-- The natural preordering on `Hole α` -/ -instance : Preorder (Hole α) where - le x y := x.left ≤ y.left - lt x y := x.left < y.left - le_refl _ := by simp - le_trans x y z h k := Preorder.le_trans _ _ _ h k - lt_iff_le_not_ge x y := Preorder.lt_iff_le_not_ge x.left y.left - -theorem lt_iff_left {x y : Hole α} : x < y ↔ x.left < y.left := Iff.rfl - -theorem le_iff_left {x y : Hole α} : x ≤ y ↔ x.left ≤ y.left := Iff.rfl - -end PartialOrder - -section LinearOrder - -variable {α : Type*} [LinearOrder α] - -theorem le_right_of_lt_left (x : Hole α) (a : α) (h : x.left < a) : x.right ≤ a := by - rw [← not_lt] - intro k - apply x.forall_notMem a ⟨h, k⟩ - -theorem le_left_of_lt_right (x : Hole α) (a : α) (h : a < x.right) : a ≤ x.left := by - rw [← not_lt] - intro k - apply x.forall_notMem a ⟨k, h⟩ - -theorem lt_iff_right {x y : Hole α} : x < y ↔ x.right < y.right := by - rw [Hole.lt_iff_left] - constructor - · intro hl - rw [← not_le] - exact fun hr ↦ x.forall_notMem y.left ⟨hl, lt_of_lt_of_le y.left_lt_right hr⟩ - · intro hr - rw [← not_le] - exact fun hl ↦ y.forall_notMem x.right ⟨lt_of_le_of_lt hl x.left_lt_right, hr⟩ - -theorem le_iff_right {x y : Hole α} : x ≤ y ↔ x.right ≤ y.right := by - simpa [Hole.le_iff_left, ← not_lt, not_iff_not] using lt_iff_right - -/-- The natural partial ordering on `Hole α` -/ -instance : PartialOrder (Hole α) where - le_antisymm x y h k := by - rw [mk.injEq] - exact ⟨le_antisymm (le_iff_left.mpr h) (le_iff_left.mpr k), - le_antisymm (le_iff_right.mp h) (le_iff_right.mp k)⟩ - -theorem left_injective : Function.Injective (fun x : Hole α ↦ x.left) := fun x y h ↦ by - rw [mk.injEq] - refine ⟨h, ?_⟩ - simp [le_antisymm_iff, ← le_iff_right, le_iff_left, h] - -theorem right_injective : Function.Injective (fun x : Hole α ↦ x.right) := fun x y h ↦ by - rw [mk.injEq] - refine ⟨?_, h⟩ - simp [le_antisymm_iff, ← le_iff_left, le_iff_right, h] - -noncomputable instance : LinearOrder (Hole α) where - le_total x t := by simp [le_iff_left, Std.le_total] - toDecidableLE := Classical.decRel LE.le - -end LinearOrder - -end Hole - -/-- The `Fill α f` of a preorder `α` replaces all `x : Hole α` with the preorder `f x` -/ -inductive Fill {α : Type*} [PartialOrder α] (f : Hole α → Type*) - | some (a : α) - | hole (x : Hole α) (t : f x) - -namespace Fill - -section lt - -variable {α : Type*} [PartialOrder α] (f : Hole α → Type*) [∀ x, LT (f x)] - -instance : LT (Fill f) where - lt - | some (a : α), some (b : α) => a < b - | some (a : α), hole y _ => a ≤ y.left - | hole x _, some b => x.right ≤ b - | hole x t, hole y u => x < y ∨ ∃ (h : y = x), t < h ▸ u - -variable {f} - -theorem some_lt_some_iff {a b : α} : (some a : Fill f) < some b ↔ a < b := Iff.rfl - -theorem some_lt_hole_iff {a : α} {y : Hole α} {u : f y} : - some a < hole y u ↔ a ≤ y.left:= Iff.rfl - -theorem hole_lt_some_iff {x : Hole α} {t : f x} {b : α} : - hole x t < some b ↔ x.right ≤ b := Iff.rfl - -theorem hole_lt_hole_iff {x y : Hole α} {t : f x} {u : f y} : - hole x t < hole y u ↔ x < y ∨ ∃ (h : y = x), t < h ▸ u := - Iff.rfl - -theorem hole_lt_hole_of_left {x y : Hole α} {t : f x} {u : f y} - (h : x < y) : hole x t < hole y u := by - simp [hole_lt_hole_iff, h] - -theorem hole_lt_hole_of_right {x : Hole α} {t u : f x} (h : t < u) : hole x t < hole x u := by - simp [hole_lt_hole_iff, h] - -end lt - -section le - -variable {α : Type*} [PartialOrder α] (f : Hole α → Type*) [∀ x, LE (f x)] - -instance : LE (Fill f) where - le - | some (a : α), some (b : α) => a ≤ b - | some (a : α), hole y _ => a ≤ y.left - | hole y _, some b => y.right ≤ b - | hole x t, hole y u => x < y ∨ ∃ (h : y = x), t ≤ h ▸ u - -theorem some_le_some_iff {a b : α} : (some a : Fill f) ≤ some b ↔ a ≤ b := Iff.rfl - -theorem some_le_hole_iff {a : α} {y : Hole α} {u : f y} : - some a ≤ hole y u ↔ a ≤ y.left:= Iff.rfl - -theorem hole_le_some_iff {x : Hole α} {t : f x} {b : α} : - hole x t ≤ some b ↔ x.right ≤ b := Iff.rfl - -theorem hole_le_hole_iff {x y : Hole α} {t : f x} {u : f y} : - hole x t ≤ hole y u ↔ x < y ∨ ∃ (h : y = x), t ≤ h ▸ u := - Iff.rfl - -theorem hole_le_hole_of_left {x y : Hole α} {t : f x} {u : f y} - (h : x < y) : hole x t ≤ hole y u := by - simp [hole_le_hole_iff, h] - -theorem hole_le_hole_iff_right {x : Hole α} {t u : f x} : - hole x t ≤ hole x u ↔ t ≤ u := by - simp [hole_le_hole_iff] - -theorem hole_le_hole_of_right {x : Hole α} {t u : f x} (h : t ≤ u) : hole x t ≤ hole x u := by - simp [hole_le_hole_iff, h] - -end le - -section partialorder - -variable {α : Type*} [PartialOrder α] {f : Hole α → Type*} [∀ x, PartialOrder (f x)] - -theorem hole_lt_hole_iff_right {x : Hole α} {t u : f x} : - hole x t < hole x u ↔ t < u := by - simp only [hole_lt_hole_iff, exists_const, or_iff_right_iff_imp, lt_irrefl x] - exact False.elim - -end partialorder - -section linear - -variable {α : Type*} [LinearOrder α] {f : Hole α → Type*} - -instance [∀ x, PartialOrder (f x)] : PartialOrder (Fill f) where - le_refl x := match x with - | some a => by simp [some_le_some_iff] - | hole x t => by simp [hole_le_hole_iff] - le_trans x y z := match x, y, z with - | some a, some b, some c => by - simp only [some_le_some_iff] - exact le_trans - | some a, hole y u, some c => by - simp only [some_le_hole_iff, hole_le_some_iff, some_le_some_iff] - intro h k - exact le_trans h (le_trans y.left_lt_right.le k) - | hole x t, some b, some c => by - simp only [hole_le_some_iff, some_le_some_iff] - exact le_trans - | hole x t, hole y u, some c => by - simp only [hole_le_hole_iff, hole_le_some_iff] - rintro (h | ⟨e, h⟩) k - · apply le_trans _ k - simp [← x.le_iff_right, h.le] - · simp [← e, k] - | some a, some b, hole z v => by - simp only [some_le_some_iff, some_le_hole_iff] - exact le_trans - | some a, hole y u, hole z v => by - simp only [some_le_hole_iff, hole_le_hole_iff] - rintro h (k | ⟨e, k⟩) - · apply le_trans h - rw [← Hole.le_iff_left] - exact k.le - · simp [e, h] - | hole x t, some b, hole z v => by - rw [hole_le_some_iff, some_le_hole_iff, hole_le_hole_iff] - intro h k - apply Or.intro_left - rw [Hole.lt_iff_left] - exact lt_of_lt_of_le x.left_lt_right (le_trans h k) - | hole x t, hole y u, hole z v => by - simp only [hole_le_hole_iff] - rintro (h | ⟨e, h⟩) (k | ⟨e', k⟩) - · left; exact lt_trans h k - · left; rwa [e'] - · left; rwa [← e] - · right - subst e' e - simp only [exists_const] at h k ⊢ - exact le_trans h k - le_antisymm x y h k := by - match x, y with - | some a, some b => - simp only [some_le_some_iff] at h k - simp only [some.injEq] - exact le_antisymm h k - | some a, hole y u => - apply False.elim - simp only [some_le_hole_iff] at h - simp only [hole_le_some_iff] at k - exact lt_irrefl a <| lt_of_le_of_lt h (lt_of_lt_of_le y.left_lt_right k) - | hole x t, some b => - apply False.elim - simp only [hole_le_some_iff] at h - simp only [some_le_hole_iff] at k - exact lt_irrefl b <| lt_of_le_of_lt k (lt_of_lt_of_le x.left_lt_right h) - | hole x t, hole y u => - rw [hole_le_hole_iff] at h k - rcases h with (h | ⟨e, h⟩) - · apply False.elim - apply lt_irrefl x - rcases k with (k | ⟨e', k⟩) - · exact lt_trans h k - · exact lt_of_lt_of_eq h e'.symm - · subst e - simp only at h - simp only [lt_self_iff_false, exists_const, false_or] at k - rw [le_antisymm h k] - lt_iff_le_not_ge x y := match x, y with - | some a, some b => by - simp only [some_lt_some_iff, some_le_some_iff] - exact lt_iff_le_not_ge - | some a, hole y u => by - rw [some_lt_hole_iff, some_le_hole_iff, hole_le_some_iff] - simp only [iff_self_and] - intro h k - exact lt_irrefl a (lt_of_le_of_lt h (lt_of_lt_of_le y.left_lt_right k)) - | hole x t, some b => by - rw [some_le_hole_iff, hole_le_some_iff, hole_lt_some_iff] - simp only [iff_self_and] - intro h k - exact lt_irrefl b (lt_of_le_of_lt k (lt_of_lt_of_le x.left_lt_right h)) - | hole x t, hole y u => by - simp only [hole_lt_hole_iff, hole_le_hole_iff] - rw [not_or, not_exists] - constructor - · rintro (h | ⟨e, h⟩) - · refine ⟨Or.intro_left _ h, Std.not_gt_of_lt h, - fun e k ↦ lt_irrefl x (lt_of_lt_of_eq h e.symm)⟩ - · refine ⟨Or.intro_right _ ⟨e, h.le⟩, e.symm.not_gt, fun _ ↦ ?_⟩ - subst e - simp only at h ⊢ - exact Std.not_le_of_gt h - · rintro ⟨(h | ⟨e, h⟩), k, k'⟩ - · apply Or.intro_left _ h - · apply Or.intro_right - subst e - simp only [lt_iff_le_not_ge, exists_const] - exact ⟨h, k' rfl⟩ - -variable [∀ x, LinearOrder (f x)] - -/-- The linear ordering on `Fill f` when `a` and all `f x` are linearly ordered -/ -noncomputable instance : LinearOrder (Fill f) where - toDecidableLE := Classical.decRel LE.le - le_total x y := match x, y with - | some a, some b => by simp only [some_le_some_iff, le_total] - | some a, hole y u => by - simp only [some_le_hole_iff, hole_le_some_iff] - apply Or.imp (h := le_or_gt a y.left) id - exact y.le_right_of_lt_left a - | hole x t, some b => by - simp only [some_le_hole_iff, hole_le_some_iff] - apply Or.imp (h := le_or_gt x.right b) id - exact Hole.le_left_of_lt_right x b - | hole x t, hole y u => by - simp only [hole_le_hole_iff] - rcases lt_trichotomy x y with (h | h | h) - · left; left; exact h - · subst h - simp [le_total] - · right; left; exact h - -instance [∀ x, Nonempty (f x)] [∀ x, NoMinOrder (f x)] [∀ x, NoMaxOrder (f x)] - [∀ x, DenselyOrdered (f x)] : DenselyOrdered (Fill f) where - dense x y h := match x, y with - | some a, some b => by - simp only [some_lt_some_iff] at h - rcases (Set.Ioo a b).eq_empty_or_nonempty with (k | ⟨⟨c, k⟩⟩) - · let x : Hole α := ⟨a, b, h, k⟩ - let t : f x := Classical.ofNonempty - refine ⟨hole x t, by simp [some_lt_hole_iff, hole_lt_some_iff, x]⟩ - · use some c - simp [some_lt_some_iff] - exact k - | some a, hole y u => by - obtain ⟨t, ht⟩ := exists_lt u - use hole y t - simp only [some_lt_hole_iff, hole_lt_hole_iff] at h ⊢ - simp [h, ht] - | hole x t, some b => by - obtain ⟨u, hu⟩ := exists_gt t - use hole x u - simp only [hole_lt_hole_iff, hole_lt_some_iff] at h ⊢ - simp [hu, h] - | hole x t, hole y u => by - simp only [hole_lt_hole_iff] at h - rcases h with (h | ⟨e, h⟩) - · obtain ⟨v, hv⟩ := exists_gt t - use hole x v - simp [hole_lt_hole_iff, h, hv] - · subst e - simp only at h - obtain ⟨v, hv, hv'⟩ := DenselyOrdered.dense t u h - use hole y v - simp [hole_lt_hole_iff, hv, hv'] - -theorem continuous_some [TopologicalSpace α] [OrderTopology α] - [∀ x, Nonempty (f x)] [∀ x, NoMinOrder (f x)] [∀ x, NoMaxOrder (f x)] - [∀ x, DenselyOrdered (f x)] - [TopologicalSpace (Fill f)] [OrderTopology (Fill f)] : - Continuous (fun a ↦ (some a : Fill f)) := by - rw [OrderTopology.continuous_iff] - intro x - simp only [isOpen_iff_nhds] - match x with - | some a => - refine ⟨fun b h ↦ ?_, fun b h ↦ ?_⟩ - · simp only [Set.mem_preimage, Set.mem_Ioi, some_lt_some_iff] at h - simp only [Filter.le_principal_iff, mem_nhds_iff] - rcases (Set.Ioo a b).eq_empty_or_nonempty with (k | ⟨⟨c, k⟩⟩) - · let x : Hole α := ⟨a, b, h, k⟩ - let t : f x := Classical.ofNonempty - refine ⟨Set.Ioi a, fun c h ↦ ?_, isOpen_Ioi, h⟩ - simp only [Set.mem_preimage, Set.mem_Ioi, some_lt_some_iff] - exact h - · refine ⟨Set.Ioi c, fun x h ↦ ?_, isOpen_Ioi, k.2⟩ - simp only [Set.mem_preimage, Set.mem_Ioi, some_lt_some_iff] - apply lt_trans k.1 h - · simp only [Set.mem_preimage, Set.mem_Iio, some_lt_some_iff] at h - simp only [Filter.le_principal_iff, mem_nhds_iff] - rcases (Set.Ioo b a).eq_empty_or_nonempty with (k | ⟨⟨c, k⟩⟩) - · let x : Hole α := ⟨b, a, h, k⟩ - let t : f x := Classical.ofNonempty - refine ⟨Set.Iio a, fun c h ↦ ?_, isOpen_Iio, h⟩ - simp only [Set.mem_preimage, Set.mem_Iio, some_lt_some_iff] - exact h - · refine ⟨Set.Iio c, fun x h ↦ ?_, isOpen_Iio, k.1⟩ - simp only [Set.mem_preimage, Set.mem_Iio, some_lt_some_iff] - apply lt_trans h k.2 - | hole x t => - refine ⟨fun a h ↦ ?_, fun a h ↦ ?_⟩ - · simp only [Set.mem_preimage, Set.mem_Ioi, hole_lt_some_iff] at h - rw [Filter.le_principal_iff, mem_nhds_iff] - refine ⟨Set.Ioi x.left, fun b k ↦ ?_, isOpen_Ioi, lt_of_lt_of_le x.left_lt_right h⟩ - simp only [Set.mem_preimage, Set.mem_Ioi, hole_lt_some_iff] - exact Hole.le_right_of_lt_left x b k - · simp only [Set.mem_preimage, Set.mem_Iio, some_lt_hole_iff] at h - rw [Filter.le_principal_iff, mem_nhds_iff] - refine ⟨Set.Iio x.right, fun b k ↦ ?_, isOpen_Iio, ?_⟩ - · simp only [Set.mem_preimage, Set.mem_Iio, some_lt_hole_iff] - exact Hole.le_left_of_lt_right x b k - · apply lt_of_le_of_lt h x.left_lt_right - -end linear - -end Fill - -end Order - -end - -/- -namespace DedekindCut - -open Set Concept - -noncomputable def embedLex [PartialOrder α] [PartialOrder β] (b : β) : - α ↪o DedekindCut (Lex (α × β)) := - RelEmbedding.trans principalEmbedding (factorEmbedding ( - ({toFun c := toLex (c, b), - inj' x y h := by simpa using h, - map_rel_iff' {x y} := by - simp [Prod.Lex.toLex_le_toLex, ← le_iff_lt_or_eq] } : α ↪o Lex (α × β)).trans - principalEmbedding)) - -variable [LinearOrder α] [TopologicalSpace α] [OrderTopology α] -variable [LinearOrder β] [TopologicalSpace β] [OrderTopology β] - [DenselyOrdered β] [NoMinOrder β] - -#synth DenselyOrdered (DedekindCut (α ×ₗβ)) -#synth CompleteLinearOrder (DedekindCut (α ×ₗβ)) - -example : @OrderTopology (DedekindCut (α ×ₗ β)) (Preorder.topology _) _ := - let := Preorder.topology (DedekindCut (Lex (α × β))) - { topology_eq_generate_intervals := rfl } - -variable [TopologicalSpace (DedekindCut (α ×ₗ β))] - [OrderTopology (DedekindCut (α ×ₗ β))] - -variable {b : β} {ι : α ↪o DedekindCut (α ×ₗ β)} - (hι : ι = embedLex b) - -example : Continuous ι := by - rw [OrderTopology.continuous_iff] - intro c - constructor - · have H (a : α) : a ∈ ι ⁻¹' Ioi c ↔ toLex (a, b) ∉ c.left := by - conv_lhs => - rw [mem_preimage, mem_Ioi] - simp [hι, embedLex] - rw [← not_le, DedekindCut.principal_le_iff] - rw [← DedekindCut.lowerBounds_right] at H - simp only [mem_lowerBounds] at H - push Not at H - rw [isOpen_iff_nhds] - intro a ha - rw [H] at ha - obtain ⟨x, hx⟩ := ha - have : ∃ u v, x = toLex (u, v) := sorry - rcases this with ⟨u, v, rfl⟩ - simp only [Prod.Lex.lt_iff, ofLex_toLex] at hx - intro F hF - simp only [Filter.mem_principal] at hF - rcases hx.2 with (h | h) - · sorry - · sorry - · sorry - -/- -noncomputable def embedBotTopLex (b : β) : - α ↪o WithBot (WithTop (DedekindCut (Lex (α × β)))) := - (RelEmbedding.trans WithTop.coeOrderHom WithBot.coeOrderHom).trans - (embedLex b).withTopMap.withBotMap --/ - -end DedekindCut --/ From 3439a43d0a4e6608ab5e958696a168e37fc4b30a Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Fri, 17 Apr 2026 22:10:19 +0200 Subject: [PATCH 19/30] remove public in import --- Mathlib/Order/Completion.lean | 3 ++- Mathlib/Topology/Sion.lean | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/Order/Completion.lean b/Mathlib/Order/Completion.lean index c4a80b8921424f..76cda616102183 100644 --- a/Mathlib/Order/Completion.lean +++ b/Mathlib/Order/Completion.lean @@ -6,7 +6,8 @@ Authors: Violeta Hernández Palacios module public import Mathlib.Order.Concept -public import Mathlib.Order.UpperLower.CompleteLattice + +import Mathlib.Order.UpperLower.CompleteLattice /-! # Dedekind-MacNeille completion diff --git a/Mathlib/Topology/Sion.lean b/Mathlib/Topology/Sion.lean index a7a699b7d4ec95..d13607a71d66ae 100644 --- a/Mathlib/Topology/Sion.lean +++ b/Mathlib/Topology/Sion.lean @@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Antoine Chambert-Loir, Anatole Dedecker -/ module - public import Mathlib.Analysis.Convex.Quasiconvex public import Mathlib.Order.SaddlePoint public import Mathlib.Topology.Instances.EReal.Lemmas +public import Mathlib.Topology.Order.Completion /-! # Formalization of Sion's version of the von Neumann minimax theorem From e9aad903262a7233c4a80991548278c71dbcc8ae Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Fri, 17 Apr 2026 22:18:03 +0200 Subject: [PATCH 20/30] add file! --- Mathlib/Topology/Order/Completion.lean | 147 +++++++++++++++++++++++++ 1 file changed, 147 insertions(+) create mode 100644 Mathlib/Topology/Order/Completion.lean diff --git a/Mathlib/Topology/Order/Completion.lean b/Mathlib/Topology/Order/Completion.lean new file mode 100644 index 00000000000000..25c862d5c91d7e --- /dev/null +++ b/Mathlib/Topology/Order/Completion.lean @@ -0,0 +1,147 @@ +/- +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 and linear order that extends `α` + +* `Order.Fill.some`: the ordered 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 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] + intro c + simp only [isOpen_iff_nhds] + refine ⟨fun a ↦ ?_, fun a ↦ ?_⟩ + · simp only [mem_preimage, mem_Ioi, Filter.le_principal_iff] + rw [lt_principal_iff] + rintro ⟨b, hb, hba⟩ + rw [mem_nhds_iff] + use Ioi b + refine ⟨fun x ↦ ?_, isOpen_Ioi, mem_Ioi.mpr hba⟩ + simp only [mem_Ioi, mem_preimage, lt_principal_iff] + exact fun h ↦ ⟨b, ⟨hb, h⟩⟩ + · simp only [mem_preimage, mem_Iio, Filter.le_principal_iff] + rw [principal_lt_iff] + rintro ⟨b, hb, hba⟩ + rw [mem_nhds_iff] + use Iio b + refine ⟨fun x ↦ ?_, isOpen_Iio, mem_Iio.mpr hba⟩ + simp only [mem_Iio, mem_preimage, principal_lt_iff] + refine fun h ↦ ⟨b, ⟨hb, h⟩⟩ + +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 α] [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 + +universe u + +theorem exists_dense_continuous_completion + (α : Type u) [LinearOrder α] [TopologicalSpace α] [OrderTopology α] : + ∃ (β : Type u) (_ : LinearOrder β) (_ : DenselyOrdered β) (_ : TopologicalSpace β) + (_ : OrderTopology β) (ι : α ↪o β), Continuous ι := by + let : TopologicalSpace (Fill α) := inferInstance + let : OrderTopology (Fill α) := inferInstance + set β := DedekindCut (Fill α) + let : TopologicalSpace β := Preorder.topology β + have orderTop : OrderTopology β := ⟨rfl⟩ + let ι : α ↪o β := Fill.some.trans DedekindCut.principalEmbedding + refine ⟨DedekindCut (Fill α), inferInstance, inferInstance, inferInstance, orderTop, + Fill.some.trans DedekindCut.principalEmbedding, ?_⟩ + simp only [RelEmbedding.coe_trans] + exact Continuous.comp DedekindCut.continuous_principal Fill.continuous_some + +end Order From d2ac476e9b9d26accd017d30f77aa7f5fa4e158d Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sat, 18 Apr 2026 00:18:42 +0200 Subject: [PATCH 21/30] remove arguments --- Mathlib/Topology/Order/Completion.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/Topology/Order/Completion.lean b/Mathlib/Topology/Order/Completion.lean index 25c862d5c91d7e..cfe08fba1e0e92 100644 --- a/Mathlib/Topology/Order/Completion.lean +++ b/Mathlib/Topology/Order/Completion.lean @@ -74,8 +74,7 @@ abbrev Fill (α : Type*) [LinearOrder α] : Type _ := namespace Fill -instance [TopologicalSpace α] [OrderTopology α] : TopologicalSpace (Fill α) := - Preorder.topology _ +instance : TopologicalSpace (Fill α) := Preorder.topology _ instance [TopologicalSpace α] [OrderTopology α] : OrderTopology (Fill α) := ⟨rfl⟩ From 0b1b164c6a4be3fc6aed1e10c3fd00473db5224f Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sat, 18 Apr 2026 00:19:37 +0200 Subject: [PATCH 22/30] remove unused import --- Mathlib/Topology/Sion.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Topology/Sion.lean b/Mathlib/Topology/Sion.lean index f72a3fbff4b532..0dd26062daebff 100644 --- a/Mathlib/Topology/Sion.lean +++ b/Mathlib/Topology/Sion.lean @@ -7,7 +7,6 @@ module public import Mathlib.Analysis.Convex.Quasiconvex public import Mathlib.Order.SaddlePoint public import Mathlib.Topology.Instances.EReal.Lemmas -public import Mathlib.Topology.Order.Completion /-! # Formalization of Sion's version of the von Neumann minimax theorem From c23a63429b2d7d9d9246157af7409239931e3761 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sat, 18 Apr 2026 01:00:30 +0200 Subject: [PATCH 23/30] update Sion after dense continuous completion --- Mathlib/Topology/Sion.lean | 160 ++++++++++--------------------------- 1 file changed, 43 insertions(+), 117 deletions(-) diff --git a/Mathlib/Topology/Sion.lean b/Mathlib/Topology/Sion.lean index f72a3fbff4b532..7ce82449e69883 100644 --- a/Mathlib/Topology/Sion.lean +++ b/Mathlib/Topology/Sion.lean @@ -13,13 +13,19 @@ public import Mathlib.Topology.Order.Completion ## Statements -`Sion.exists_isSaddlePointOn` : Let `X` and `Y` be convex subsets of topological vector spaces `E` and `F`, -`X` being moreover compact, -and let `f : X × Y → ℝ` be a function such that +`X` being moreover compact, `β` a linearly ordered set (with the order topology), +and let `f : X × Y → β` be a function such that - for all `x ∈ X`, `f(x, ⬝)` is upper semicontinuous and quasiconcave - for all `y ∈ Y`, `f(⬝, y)` is lower semicontinuous and quasiconvex -Then `⊓ x, ⊔ y, f (x, y) = ⊔ y, ⊓ x f (x, y)`. + +* `Sion.minimax' : If `β` is complete, then `⊓ x, ⊔ y, f (x, y) = ⊔ y, ⊓ x f (x, y)`. + +* `Sion.minimax` : A variant using `IsLUB` and `IsGLB` that does not assume a complete order. + +* `Sion.exists_isSaddlePointOn` : There exists `a ∈ X` and `b ∈ Y` such that + `Function.uncurry f` has a saddle point at `(a, b)`, that is, + `f a y ≤ f x b` for all `x ∈ X` and `y ∈ Y`. The classical case of the theorem assumes that `f` is continuous, `f(x, ⬝)` is concave, `f(⬝, y)` is convex. @@ -27,29 +33,21 @@ The classical case of the theorem assumes that `f` is continuous, As a particular case, one get the von Neumann theorem where `f` is bilinear and `E`, `F` are finite dimensional. +* `Sion.minimax` is a variant of that result that +avoids complete linear orders using `IsLUB` and `IsGLB`. + We follow the proof of [Komiya-1988][Komiya (1988)]. ## Remark on implementation - * The essential part of the proof holds for a function - `f : X → Y → β`, where `β` is a complete dense linear order. - * We have written part of it for just a dense linear order, - - * On the other hand, if the theorem holds for such `β`, - it must hold for any linear order, for the reason that - any linear order embeds into a complete dense linear order. - Although one can construct such an embedding using the Dedekind-Mac Neille completion, - this result does not seem to be known to Mathlib. - - * When `β` is `ℝ`, one can use `Real.toEReal` and one gets a proof for `ℝ`. +* The initial proof in [Komiya-1988][Komiya (1988)] is written for `β := ℝ` + but it holds verbatim for any dense linearly ordered set. + Using `Order.exists_dense_continuous_completion`, it applies to any linear order. ## TODO - Spell out the particular case of von Neumann theorem. -- Use the Dedekind MacNeille completion of a linear order to simplify - the statement of `DMCompletion.exists_isSaddlePointOn`. - ## References - [vonNeumann-1928][Neumann, John von (1928). @@ -229,11 +227,11 @@ theorem isClosed_setOf_sublevelLeft_subset exact ⟨⟨z', hz'⟩, ⟨hxz'2, hxz'1⟩⟩ exact hfx.mp <| .of_forall fun z hzt' ⟨hz, hz'⟩ ↦ ⟨hz, ⟨hzt'.le, hz'⟩⟩ -variable [DenselyOrdered β] variable [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] +-- Provisional version that assumes `DenselyOrdered β` include ne_X kX hfx hfx' cY hfy hfy' in -public theorem exists_lt_iInf_of_lt_iInf_of_sup +theorem exists_lt_iInf_of_lt_iInf_of_sup' [DenselyOrdered β] {y1 : F} (hy1 : y1 ∈ Y) {y2 : F} (hy2 : y2 ∈ Y) {t : β} (ht : ∀ x ∈ X, t < f x y1 ⊔ f x y2) : ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0 := by @@ -286,6 +284,29 @@ public theorem exists_lt_iInf_of_lt_iInf_of_sup · refine hJ1J2 ⟨y1, left_mem_segment ℝ (y1 : F) y2⟩ ⟨?_, h2 (Set.mem_univ _)⟩ grw [mem_J1_iff, monotone_sublevelLeft y1 htt'.le] +include ne_X kX hfx hfx' cY hfy hfy' in +public theorem exists_lt_iInf_of_lt_iInf_of_sup + {y1 : F} (hy1 : y1 ∈ Y) {y2 : F} (hy2 : y2 ∈ Y) {t : β} + (ht : ∀ x ∈ X, t < f x y1 ⊔ f x y2) : + ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0 := by + let : TopologicalSpace β := Preorder.topology _ + have : OrderTopology β := ⟨rfl⟩ + obtain ⟨γ, _, _, _, _, ι, hι⟩ := Order.exists_dense_continuous_completion β + let g := fun x y ↦ ι (f x y) + have hgy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ g x y) X := fun y hy ↦ + hι.comp_lowerSemicontinuousOn (hfy y hy) ι.monotone + have hgy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ g x y := fun y hy ↦ + (hfy' y hy).monotone_comp ι.monotone + have hgx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ g x y) Y := fun x hx ↦ + hι.comp_upperSemicontinuousOn (hfx x hx) ι.monotone + have hgx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ g x y := fun x hx ↦ + (hfx' x hx).monotone_comp ι.monotone + have ht' : ∀ x ∈ X, ι t < g x y1 ⊔ g x y2 := fun x hx ↦ by + simp only [g, ← SupHomClass.map_sup, ι.lt_iff_lt.mpr (ht x hx)] + obtain ⟨y0, hy0, h⟩ := Sion.exists_lt_iInf_of_lt_iInf_of_sup' + ne_X kX hgy hgy' cY hgx hgx' hy1 hy2 ht' + refine ⟨y0, hy0, by simpa [g, ι.lt_iff_lt] using h⟩ + variable (cX : Convex ℝ X) include ne_X cX cY kX hfx hfx' hfy hfy' in @@ -399,7 +420,7 @@ public theorem minimax variable (ne_Y : Y.Nonempty) (kY : IsCompact Y) include ne_X ne_Y cX cY kX kY hfx hfx' hfy hfy' in /-- The Sion-von Neumann minimax theorem (saddle point form) -/ -public theorem exists_isSaddlePointOn' : +public theorem exists_isSaddlePointOn : ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b := by have hmax_y (x) (hx : x ∈ X) : ∃ y ∈ Y, IsMaxOn (f x) Y y := (hfx x hx).exists_isMaxOn ne_Y kY choose! η η_mem η_max using hmax_y @@ -426,7 +447,7 @@ end LinearOrder section CompleteLinearOrder -variable {E F β : Type*} [CompleteLinearOrder β] [DenselyOrdered β] +variable {E F β : Type*} [CompleteLinearOrder β] variable {X : Set E} {Y : Set F} {f : E → F → β} variable [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] @@ -446,101 +467,6 @@ public theorem minimax' : (⨅ x ∈ X, ⨆ y ∈ Y, f x y) = ⨆ y ∈ Y, ⨅ x minimax ne_X kX hfy hfy' cY hfx hfx' cX _ (fun _ _ ↦ isLUB_biSup) _ isGLB_biInf _ (fun _ _ ↦ isGLB_biInf) _ isLUB_biSup -include ne_X ne_Y cX cY kX kY hfx hfx' hfy hfy' in -/-- The Sion-von Neumann minimax theorem (saddle point form), -case of complete linear orders. -/ -public theorem exists_saddlePointOn' : - ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b := by - have hlsc : LowerSemicontinuousOn (fun x => ⨆ y ∈ Y, f x y) X := fun x hx ↦ by - apply lowerSemicontinuousWithinAt_iSup - intro i - exact lowerSemicontinuousWithinAt_iSup fun i_1 ↦ hfy i i_1 x hx - have husc : UpperSemicontinuousOn (fun y => ⨅ x ∈ X, f x y) Y := fun y hy ↦ by - apply upperSemicontinuousWithinAt_iInf - intro i - exact upperSemicontinuousWithinAt_iInf fun i_1 ↦ hfx i i_1 y hy - obtain ⟨a, ha, ha'⟩ := LowerSemicontinuousOn.exists_isMinOn - ne_X kX hlsc - obtain ⟨b, hb, hb'⟩ := UpperSemicontinuousOn.exists_isMaxOn ne_Y kY husc - use a, ha, b, hb - rw [isSaddlePointOn_iff' ha hb] - refine le_trans (le_iInf₂ ha') ?_ - refine le_trans ?_ (iSup₂_le_iff.mpr hb') - rw [minimax' ne_X cX kX hfy hfy' cY hfx hfx'] - end CompleteLinearOrder -section DedekindMacNeille - -variable {E F β γ : Type*} [LinearOrder β] - -variable {X : Set E} {Y : Set F} {f : E → F → β} -variable [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] - [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] - (ne_X : X.Nonempty) (cX : Convex ℝ X) (kX : IsCompact X) - (hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x : E ↦ f x y) X) - (hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) - -variable [TopologicalSpace F] [AddCommGroup F] [Module ℝ F] - [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] - (cY : Convex ℝ Y) (ne_Y : Y.Nonempty) (kY : IsCompact Y) - (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 densely ordered completion. -(The Dedekind MacNeille completion is not densely ordered.) -/ -variable [TopologicalSpace β] [OrderTopology β] -variable {γ : Type*} [CompleteLinearOrder γ] [DenselyOrdered γ] - [TopologicalSpace γ] [OrderTopology γ] - {ι : β ↪o γ} (hι : Continuous ι) - -include ne_X ne_Y cX cY kX kY hfx hfx' hfy hfy' hι in -/-- The minimax theorem, in the saddle point form, -when `β` is given a Dedekind-MacNeille completion `ι : β ↪o γ` -/ -public theorem DMCompletion.exists_isSaddlePointOn : - ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b := by - -- Reduce to the cae of EReal-valued functions - let φ : E → F → γ := fun x y ↦ ι (f x y) - -- suffices : ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y φ a b - have hφx (x) (hx : x ∈ X) : UpperSemicontinuousOn (fun y ↦ φ x y) Y := by - convert Continuous.comp_upperSemicontinuousOn hι (hfx x hx) ι.monotone - have hφx' (x) (hx : x ∈ X) : QuasiconcaveOn ℝ Y fun y ↦ φ x y := by - convert (hfx' x hx).monotone_comp ι.monotone - have hφy (y) (hy : y ∈ Y) : LowerSemicontinuousOn (fun x ↦ φ x y) X := by - convert Continuous.comp_lowerSemicontinuousOn hι (hfy y hy) ι.monotone - have hφy' (y) (hy : y ∈ Y) : QuasiconvexOn ℝ X fun x ↦ φ x y := by - convert (hfy' y hy).monotone_comp ι.monotone - obtain ⟨a, ha, b, hb, hab⟩ := - exists_isSaddlePointOn' ne_X kX hφy hφy' cY kY hφx hφx' cX ne_Y - use a, ha, b, hb - intro x hx y hy - simpa only [OrderEmbedding.le_iff_le, φ] using hab x hx y hy - -end DedekindMacNeille - -section Real - -variable {E F : Type*} -variable {X : Set E} {Y : Set F} {f : E → F → ℝ} -variable [TopologicalSpace E] [AddCommGroup E] [Module ℝ E] - [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] - (ne_X : X.Nonempty) (cX : Convex ℝ X) (kX : IsCompact X) - (hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x : E ↦ f x y) X) - (hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) - -variable [TopologicalSpace F] [AddCommGroup F] [Module ℝ F] - [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] - (cY : Convex ℝ Y) (ne_Y : Y.Nonempty) (kY : IsCompact Y) - (hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y : F => f x y) Y) - (hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) - -include ne_X ne_Y cX cY kX kY hfx hfx' hfy hfy' in -/-- The minimax theorem, in the saddle point form -/ -public theorem exists_isSaddlePointOn : - ∃ a ∈ X, ∃ b ∈ Y, IsSaddlePointOn X Y f a b := - DMCompletion.exists_isSaddlePointOn ne_X cX kX hfy hfy' cY ne_Y kY hfx hfx' - (ι := EReal.orderEmbedding) (hι := continuous_coe_real_ereal) - -end Real - end Sion From bf4dadc2ec2674aa1521bf6121cbeb1ec06f1303 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sat, 18 Apr 2026 12:22:19 +0200 Subject: [PATCH 24/30] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Violeta Hernández Palacios --- Mathlib/Topology/Order/Completion.lean | 88 ++++++++++---------------- 1 file changed, 32 insertions(+), 56 deletions(-) diff --git a/Mathlib/Topology/Order/Completion.lean b/Mathlib/Topology/Order/Completion.lean index cfe08fba1e0e92..0371c689f59195 100644 --- a/Mathlib/Topology/Order/Completion.lean +++ b/Mathlib/Topology/Order/Completion.lean @@ -8,61 +8,46 @@ 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 and linear order that extends `α` - -* `Order.Fill.some`: the ordered 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 a dense and complete linear order. - +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 α] +variable {α : Type*} [LinearOrder α] + theorem DedekindCut.continuous_principal [TopologicalSpace α] [OrderTopology α] [TopologicalSpace (DedekindCut α)] [OrderTopology (DedekindCut α)] : Continuous (fun a : α ↦ principal a) := by rw [OrderTopology.continuous_iff] - intro c - simp only [isOpen_iff_nhds] - refine ⟨fun a ↦ ?_, fun a ↦ ?_⟩ - · simp only [mem_preimage, mem_Ioi, Filter.le_principal_iff] - rw [lt_principal_iff] - rintro ⟨b, hb, hba⟩ - rw [mem_nhds_iff] - use Ioi b - refine ⟨fun x ↦ ?_, isOpen_Ioi, mem_Ioi.mpr hba⟩ - simp only [mem_Ioi, mem_preimage, lt_principal_iff] - exact fun h ↦ ⟨b, ⟨hb, h⟩⟩ - · simp only [mem_preimage, mem_Iio, Filter.le_principal_iff] - rw [principal_lt_iff] - rintro ⟨b, hb, hba⟩ - rw [mem_nhds_iff] - use Iio b - refine ⟨fun x ↦ ?_, isOpen_Iio, mem_Iio.mpr hba⟩ - simp only [mem_Iio, mem_preimage, principal_lt_iff] - refine fun h ↦ ⟨b, ⟨hb, h⟩⟩ + 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 @@ -131,16 +116,7 @@ universe u theorem exists_dense_continuous_completion (α : Type u) [LinearOrder α] [TopologicalSpace α] [OrderTopology α] : ∃ (β : Type u) (_ : LinearOrder β) (_ : DenselyOrdered β) (_ : TopologicalSpace β) - (_ : OrderTopology β) (ι : α ↪o β), Continuous ι := by - let : TopologicalSpace (Fill α) := inferInstance - let : OrderTopology (Fill α) := inferInstance - set β := DedekindCut (Fill α) - let : TopologicalSpace β := Preorder.topology β - have orderTop : OrderTopology β := ⟨rfl⟩ - let ι : α ↪o β := Fill.some.trans DedekindCut.principalEmbedding - refine ⟨DedekindCut (Fill α), inferInstance, inferInstance, inferInstance, orderTop, - Fill.some.trans DedekindCut.principalEmbedding, ?_⟩ - simp only [RelEmbedding.coe_trans] - exact Continuous.comp DedekindCut.continuous_principal Fill.continuous_some + (_ : OrderTopology β) (ι : α ↪o β), Continuous ι := + ⟨_, inferInstance, inferInstance, inferInstance, inferInstance, _, Fill.continuous_some⟩ end Order From d092afa53bdee0ce09abfd551e83774d0e2abdbf Mon Sep 17 00:00:00 2001 From: "pre-commit-ci-lite[bot]" <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Date: Sat, 18 Apr 2026 10:22:58 +0000 Subject: [PATCH 25/30] [pre-commit.ci lite] apply automatic fixes --- Mathlib/Topology/Order/Completion.lean | 64 +++++++++++++------------- 1 file changed, 32 insertions(+), 32 deletions(-) diff --git a/Mathlib/Topology/Order/Completion.lean b/Mathlib/Topology/Order/Completion.lean index 0371c689f59195..c031e1e0c0dbb9 100644 --- a/Mathlib/Topology/Order/Completion.lean +++ b/Mathlib/Topology/Order/Completion.lean @@ -8,46 +8,46 @@ 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. +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 α] - +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] + 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 @@ -116,7 +116,7 @@ universe u theorem exists_dense_continuous_completion (α : Type u) [LinearOrder α] [TopologicalSpace α] [OrderTopology α] : ∃ (β : Type u) (_ : LinearOrder β) (_ : DenselyOrdered β) (_ : TopologicalSpace β) - (_ : OrderTopology β) (ι : α ↪o β), Continuous ι := - ⟨_, inferInstance, inferInstance, inferInstance, inferInstance, _, Fill.continuous_some⟩ + (_ : OrderTopology β) (ι : α ↪o β), Continuous ι := + ⟨_, inferInstance, inferInstance, inferInstance, inferInstance, _, Fill.continuous_some⟩ end Order From 62408bf68a3062b2c7b6c956e607763f22068dd0 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sat, 18 Apr 2026 12:27:09 +0200 Subject: [PATCH 26/30] adjust --- Mathlib/Topology/Sion.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Topology/Sion.lean b/Mathlib/Topology/Sion.lean index 0dd26062daebff..c533217f496c1a 100644 --- a/Mathlib/Topology/Sion.lean +++ b/Mathlib/Topology/Sion.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Antoine Chambert-Loir, Anatole Dedecker -/ module + public import Mathlib.Analysis.Convex.Quasiconvex public import Mathlib.Order.SaddlePoint public import Mathlib.Topology.Instances.EReal.Lemmas @@ -487,7 +488,7 @@ variable [TopologicalSpace F] [AddCommGroup F] [Module ℝ F] (hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) /- The following lines essentially assume that `β` has a densely ordered completion. -(The Dedekind MacNeille completion is not densely ordered.) -/ +(The Dedekind MacNeille completion is not densely ordered unless `β` is.) -/ variable [TopologicalSpace β] [OrderTopology β] variable {γ : Type*} [CompleteLinearOrder γ] [DenselyOrdered γ] [TopologicalSpace γ] [OrderTopology γ] From 8fd05a100471ddcac142c37847cbf347c0c30e96 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sat, 18 Apr 2026 12:32:58 +0200 Subject: [PATCH 27/30] replace completion --- Mathlib/Topology/Order/Completion.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/Mathlib/Topology/Order/Completion.lean b/Mathlib/Topology/Order/Completion.lean index c031e1e0c0dbb9..8aa189003abfef 100644 --- a/Mathlib/Topology/Order/Completion.lean +++ b/Mathlib/Topology/Order/Completion.lean @@ -113,10 +113,15 @@ 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) (_ : LinearOrder β) (_ : DenselyOrdered β) (_ : TopologicalSpace β) + ∃ (β : Type u) (_ : CompleteLinearOrder β) (_ : DenselyOrdered β) (_ : TopologicalSpace β) (_ : OrderTopology β) (ι : α ↪o β), Continuous ι := - ⟨_, inferInstance, inferInstance, inferInstance, inferInstance, _, Fill.continuous_some⟩ + 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 From b89d78512f32aa0d72ebae048a518715aa5f056c Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Sun, 19 Apr 2026 14:43:58 +0200 Subject: [PATCH 28/30] adjust import --- Mathlib/Topology/Sion.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/Topology/Sion.lean b/Mathlib/Topology/Sion.lean index 04e3c841fa8b94..196cda344115c3 100644 --- a/Mathlib/Topology/Sion.lean +++ b/Mathlib/Topology/Sion.lean @@ -7,7 +7,8 @@ module public import Mathlib.Analysis.Convex.Quasiconvex public import Mathlib.Order.SaddlePoint -public import Mathlib.Topology.Instances.EReal.Lemmas +public import Mathlib.Topology.Order.Completion +public import Mathlib.Topology.Semicontinuity.Basic /-! # Formalization of Sion's version of the von Neumann minimax theorem @@ -305,7 +306,7 @@ public theorem exists_lt_iInf_of_lt_iInf_of_sup simp only [g, ← SupHomClass.map_sup, ι.lt_iff_lt.mpr (ht x hx)] obtain ⟨y0, hy0, h⟩ := Sion.exists_lt_iInf_of_lt_iInf_of_sup' ne_X kX hgy hgy' cY hgx hgx' hy1 hy2 ht' - refine ⟨y0, hy0, by simpa [g, ι.lt_iff_lt] using h⟩ + exact ⟨y0, hy0, by simpa [g, ι.lt_iff_lt] using h⟩ variable (cX : Convex ℝ X) From 141eefa371bf0b7cf25da491fd55f6800ef41049 Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Mon, 20 Apr 2026 10:55:19 +0200 Subject: [PATCH 29/30] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Violeta Hernández Palacios Co-authored-by: Antoine Chambert-Loir --- Mathlib/Topology/Sion.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Topology/Sion.lean b/Mathlib/Topology/Sion.lean index 196cda344115c3..8423c432dd178b 100644 --- a/Mathlib/Topology/Sion.lean +++ b/Mathlib/Topology/Sion.lean @@ -19,6 +19,7 @@ Let `X` and `Y` be convex subsets of topological vector spaces `E` and `F`, and let `f : X × Y → β` be a function such that - for all `x ∈ X`, `f(x, ⬝)` is upper semicontinuous and quasiconcave - for all `y ∈ Y`, `f(⬝, y)` is lower semicontinuous and quasiconvex +Then: * `Sion.minimax' : If `β` is complete, then `⊓ x, ⊔ y, f (x, y) = ⊔ y, ⊓ x f (x, y)`. @@ -35,7 +36,7 @@ As a particular case, one get the von Neumann theorem where `f` is bilinear and `E`, `F` are finite dimensional. * `Sion.minimax` is a variant of that result that -avoids complete linear orders using `IsLUB` and `IsGLB`. + avoids complete linear orders using `IsLUB` and `IsGLB`. We follow the proof of [Komiya-1988][Komiya (1988)]. From 423ae94c4ad9d6de75b106ed4c559f161edb33a4 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci-lite[bot]" <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Date: Mon, 20 Apr 2026 08:56:00 +0000 Subject: [PATCH 30/30] [pre-commit.ci lite] apply automatic fixes --- Mathlib/Topology/Sion.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Topology/Sion.lean b/Mathlib/Topology/Sion.lean index 8423c432dd178b..d566ed79a05369 100644 --- a/Mathlib/Topology/Sion.lean +++ b/Mathlib/Topology/Sion.lean @@ -36,7 +36,7 @@ As a particular case, one get the von Neumann theorem where `f` is bilinear and `E`, `F` are finite dimensional. * `Sion.minimax` is a variant of that result that - avoids complete linear orders using `IsLUB` and `IsGLB`. + avoids complete linear orders using `IsLUB` and `IsGLB`. We follow the proof of [Komiya-1988][Komiya (1988)].