merge

Author: vihdzp

Mathlib.lean

@@ -5914,7 +5914,8 @@ 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.DirSupClosed
+public import Mathlib.Order.DirSupClosed.Basic
+public import Mathlib.Order.DirSupClosed.Finite
 public import Mathlib.Order.Directed
 public import Mathlib.Order.DirectedInverseSystem
 public import Mathlib.Order.Disjoint

Mathlib/Order/DirSupClosed.lean Mathlib/Order/DirSupClosed/Basic.leanMathlib/Order/DirSupClosed.lean renamed to Mathlib/Order/DirSupClosed/Basic.lean

@@ -5,12 +5,11 @@ Authors: Christopher Hoskin, Violeta Hernández Palacios
 -/
 module
 
-public import Mathlib.Data.Fintype.Order
 public import Mathlib.Order.Antisymmetrization
 public import Mathlib.Order.CompleteLattice.Defs
 public import Mathlib.Order.UpperLower.Basic
 
-import Mathlib.Data.Nat.Lattice
+import Mathlib.Data.Set.Lattice
 
 /-!
 # Sets closed under directed suprema
@@ -292,37 +291,18 @@ end Preorder
 section PartialOrder
 variable [PartialOrder α]
 
-theorem dirSupClosed_singleton (a : α) : DirSupClosed {a} := by
+theorem DirSupClosed.singleton (a : α) : DirSupClosed {a} := by
   intro d hda hdn _ b hb
   rw [hdn.subset_singleton_iff] at hda
   subst hda
   exact mem_singleton_of_eq (hb.unique isLUB_singleton)
 
-theorem dirSupClosedOn_singleton (a : α) : DirSupClosedOn D {a} :=
-  (dirSupClosed_singleton a).dirSupClosedOn
-
-theorem Set.Finite.dirSupClosed (hs : s.Finite) : DirSupClosed s := by
-  intro t ht ht₀ ht₁ a ha
-  obtain ⟨b, hbt, hb⟩ := ht₁.finite_le ht₀ (hs.subset ht)
-  exact ht <| ha.unique ⟨hb, fun x hx ↦ hx hbt⟩ ▸ hbt
-
-theorem dirSupClosed_range_nat {f : ℕ → α} (hf : Monotone f) (hf' : IsCofinal (.range f)) :
-    DirSupClosed (range f) := by
-  intro s hs hs₀ hs₁ a ha
-  obtain ⟨_, ⟨n, rfl⟩, han⟩ := hf' a
-  obtain rfl | han := han.eq_or_lt
-  · simp
-  have hfb : BddAbove (f ⁻¹' s) := by
-    refine ⟨n, fun m hm ↦ ?_⟩
-    by_contra! hnm
-    exact (ha.1 hm).not_gt (han.trans_le (hf hnm.le))
-  refine ⟨sSup (f ⁻¹' s), IsLUB.unique ⟨?_, ?_⟩ ha⟩ <;> intro x hx
-  · obtain ⟨m, rfl⟩ := hs hx
-    exact hf (le_csSup hfb hx)
-  · apply hx (Nat.sSup_mem _ hfb)
-    obtain ⟨x, hx⟩ := hs₀
-    obtain ⟨m, rfl⟩ := hs hx
-    exact ⟨m, hx⟩
+@[deprecated (since := "2026-05-22")] alias dirSupClosed_singleton := DirSupClosed.singleton
+
+theorem DirSupClosedOn.singleton (a : α) : DirSupClosedOn D {a} :=
+  (DirSupClosed.singleton a).dirSupClosedOn
+
+@[deprecated (since := "2026-05-22")] alias dirSupClosedOn_singleton := DirSupClosedOn.singleton
 
 end PartialOrder
 

Mathlib/Order/DirSupClosed/Finite.lean

@@ -0,0 +1,44 @@
+/-
+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
+-/
+module
+
+public import Mathlib.Data.Set.Finite.Basic
+public import Mathlib.Order.DirSupClosed.Basic
+
+import Mathlib.Data.Nat.Lattice
+
+/-!
+# Finite sets are closed under suprema
+-/
+
+public section
+
+variable {α : Type*} [PartialOrder α]
+
+theorem Set.Finite.dirSupClosed {s : Set α} (hs : s.Finite) : DirSupClosed s := by
+  induction s, hs using induction_on with
+  | empty => exact .empty
+  | insert has _ hs₁ =>
+    rw [Set.insert_eq]
+    exact (DirSupClosed.singleton _).union hs₁
+
+theorem dirSupClosed_range_nat {f : ℕ → α} (hf : Monotone f) (hf' : IsCofinal (.range f)) :
+    DirSupClosed (.range f) := by
+  intro s hs hs₀ hs₁ a ha
+  obtain ⟨_, ⟨n, rfl⟩, han⟩ := hf' a
+  obtain rfl | han := han.eq_or_lt
+  · simp
+  have hfb : BddAbove (f ⁻¹' s) := by
+    refine ⟨n, fun m hm ↦ ?_⟩
+    by_contra! hnm
+    exact (ha.1 hm).not_gt (han.trans_le (hf hnm.le))
+  refine ⟨sSup (f ⁻¹' s), IsLUB.unique ⟨?_, ?_⟩ ha⟩ <;> intro x hx
+  · obtain ⟨m, rfl⟩ := hs hx
+    exact hf (le_csSup hfb hx)
+  · apply hx (Nat.sSup_mem _ hfb)
+    obtain ⟨x, hx⟩ := hs₀
+    obtain ⟨m, rfl⟩ := hs hx
+    exact ⟨m, hx⟩

Mathlib/Order/IsNormal.lean

@@ -6,7 +6,7 @@ Authors: Violeta Hernández Palacios
 module
 
 public import Mathlib.Dynamics.FixedPoints.Defs
-public import Mathlib.Order.DirSupClosed
+public import Mathlib.Order.DirSupClosed.Basic
 public import Mathlib.Order.SuccPred.CompleteLinearOrder
 public import Mathlib.Order.SuccPred.InitialSeg
 

Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean

@@ -9,6 +9,8 @@ public import Mathlib.SetTheory.Cardinal.Arithmetic
 public import Mathlib.SetTheory.Cardinal.Cofinality.Basic
 public import Mathlib.SetTheory.Ordinal.FixedPoint
 
+import Mathlib.Order.DirSupClosed.Finite
+
 /-!
 # Cofinality of an ordinal
 
@@ -202,7 +204,7 @@ theorem dirSupClosed_of_type_le_omega0 [LinearOrder α] [WellFoundedLT α]
     apply Finite.dirSupClosed
     rw [Set.Finite, ← mk_lt_aleph0_iff]
     simp_all
-  · let e : ℕ ≃o s := by
+  · have e : ℕ ≃o s := by
       rw [omega0, ← lift_id (type _), lift_type_eq] at hω
       exact OrderIso.ofRelIsoLT hω.some.symm
     have hfs : .range (Subtype.val ∘ e) = s := by simp

Mathlib/Topology/Order/ScottTopology.lean

@@ -5,7 +5,7 @@ Authors: Christopher Hoskin
 -/
 module
 
-public import Mathlib.Order.DirSupClosed
+public import Mathlib.Order.DirSupClosed.Basic
 public import Mathlib.Order.ScottContinuity
 public import Mathlib.Topology.Order.UpperLowerSetTopology