begin

Author: vihdzp

Mathlib.lean

@@ -5916,7 +5916,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/Data/Fintype/Order.lean

@@ -195,6 +195,14 @@ lemma Directed.finite_le {ι κ : Sort*} [Nonempty ι] [Finite κ] {f : ι → 
   simpa using
     (hf.comp_of_surjective PLift.down_surjective).finite_set_le (Set.finite_range (PLift.up ∘ g))
 
+theorem DirectedOn.finite_le {s : Set α} (hs₀ : s.Nonempty) (D : DirectedOn r s)
+    (hs : s.Finite) : ∃ z ∈ s, ∀ i ∈ s, r i z := by
+  have := hs₀.to_subtype
+  have := hs.to_subtype
+  obtain ⟨⟨z, hzs⟩, hz⟩ := D.directed_val.finite_le id
+  use z, hzs
+  simpa using hz
+
 variable [Nonempty α] [Preorder α]
 
 theorem Finite.exists_le [IsDirectedOrder α] (f : β → α) : ∃ M, ∀ i, f i ≤ M :=

Mathlib/Data/Set/Image.lean

@@ -955,6 +955,11 @@ theorem preimage_rangeSplitting {f : α → β} (hf : Injective f) :
   (image_eq_preimage_of_inverse (rightInverse_rangeSplitting hf)
       (leftInverse_rangeSplitting f)).symm
 
+theorem rangeSplitting_strictMono [LinearOrder α] [PartialOrder β] {f : α → β} (hf : Monotone f) :
+    StrictMono (rangeSplitting f) := by
+  refine fun x y h ↦ hf.reflect_lt ?_
+  simpa [apply_rangeSplitting f]
+
 theorem isCompl_range_some_none (α : Type*) : IsCompl (range (some : α → Option α)) {none} :=
   IsCompl.of_le (fun _ ⟨⟨_, ha⟩, (hn : _ = none)⟩ => Option.some_ne_none _ (ha.trans hn))
     fun x _ => Option.casesOn x (Or.inr rfl) fun _ => Or.inl <| mem_range_self _

Mathlib/Order/Cofinal.lean

@@ -52,6 +52,11 @@ theorem IsCofinal.mono {s t : Set α} (h : s ⊆ t) (hs : IsCofinal s) : IsCofin
   obtain ⟨b, hb, hb'⟩ := hs a
   exact ⟨b, h hb, hb'⟩
 
+theorem IsCofinal.nonempty [Nonempty α] {s : Set α} (h : IsCofinal s) : s.Nonempty := by
+  inhabit α
+  obtain ⟨x, hx, _⟩ := h default
+  exact ⟨x, hx⟩
+
 end LE
 
 section Preorder

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

@@ -288,17 +288,21 @@ lemma dirSupInaccOn_Iic (a : α) : DirSupInaccOn D (Iic a) :=
 
 end Preorder
 
-namespace PartialOrder
+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
+@[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/Club.lean

@@ -5,15 +5,16 @@ Authors: Violeta Hernández Palacios
 -/
 module
 
-public import Mathlib.Order.DirSupClosed
 public import Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
 
 /-!
 # Club sets
 
-A subset of a well-ordered type `α` is called a club set when it is closed in the order topology and
-cofinal. If `α` has no maximum, then an equivalent condition is that `α` is closed and unbounded;
-hence the name.
+A subset of a well-ordered type `α` is called a **club set** when it is closed in the order topology
+and cofinal. If `α` has no maximum, then an equivalent condition is that `α` is closed and
+unbounded; hence the name.
+
+A **stationary set** is a set which intersects all club sets.
 
 ## Implementation notes
 
@@ -28,6 +29,8 @@ universe u v
 
 open Cardinal Order Ordinal Set
 
+variable {α : Type v} {s t : Set α} {x : α} [LinearOrder α]
+
 /-- A club set is closed under suprema and cofinal. -/
 structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where
   /-- Club sets are closed under suprema. If `α` is a well-order with the order topology, this
@@ -39,8 +42,6 @@ structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where
 
 namespace IsClub
 
-variable {α : Type v} {s t : Set α} {x : α} [LinearOrder α]
-
 @[simp]
 theorem of_isEmpty [IsEmpty α] {s : Set α} : IsClub s :=
   ⟨.of_isEmpty, .of_isEmpty⟩
@@ -49,6 +50,12 @@ theorem of_isEmpty [IsEmpty α] {s : Set α} : IsClub s :=
 protected theorem univ : IsClub (α := α) .univ :=
   ⟨.univ, .univ⟩
 
+protected theorem nonempty [Nonempty α] (hs : IsClub s) : s.Nonempty :=
+  hs.isCofinal.nonempty
+
+theorem _root_.isClub_empty_iff : IsClub (α := α) ∅ ↔ IsEmpty α :=
+  ⟨fun h ↦ isCofinal_empty_iff.1 h.isCofinal, fun _ ↦ .of_isEmpty⟩
+
 protected theorem union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) :=
   ⟨hs.dirSupClosed.union ht.dirSupClosed, hs.isCofinal.mono subset_union_left⟩
 
@@ -83,7 +90,6 @@ theorem iInter_of_cof_le_one {ι : Type*} {f : ι → Set α} (hα : cof α ≤
   exact .sInter_of_cof_le_one hα (by simpa)
 
 section WellFoundedLT
-
 variable [WellFoundedLT α]
 
 attribute [local instance]
@@ -117,14 +123,22 @@ protected theorem iInter {ι : Type u} {f : ι → Set α} (hα : cof α ≠ ℵ
   rw [← Cardinal.lift_lt]
   exact mk_range_le_lift.trans_lt hι
 
-protected theorem inter {s t : Set α} (hα : cof α ≠ ℵ₀) (hs : IsClub s) (ht : IsClub t) :
-    IsClub (s ∩ t) := by
-  rw [← sInter_pair]
-  have H : ∀ x ∈ ({s, t} : Set _), IsClub x := by simpa [hs]
-  obtain hα | hα' := hα.lt_or_gt
-  · rw [cof_lt_aleph0_iff] at hα
-    exact .sInter_of_cof_le_one hα H
-  · exact .sInter hα (hα'.trans_le' <| by simp) H
+theorem sInter_of_countable {s : Set (Set α)} (hα : cof α ≠ ℵ₀) (hsα : s.Countable)
+    (hs : ∀ x ∈ s, IsClub x) : IsClub (⋂₀ s) := by
+  obtain hα | hα := hα.lt_or_gt
+  · apply IsClub.sInter_of_cof_le_one _ hs
+    rwa [← Order.cof_lt_aleph0_iff]
+  · apply IsClub.sInter hα.ne' (hα.trans_le' _) hs
+    rwa [le_aleph0_iff_set_countable]
+
+theorem iInter_of_countable {ι : Type*} {f : ι → Set α} [Countable ι] (hα : cof α ≠ ℵ₀)
+    (hf : ∀ i, IsClub (f i)) : IsClub (⋂ i, f i) := by
+  rw [← sInter_range]
+  apply IsClub.sInter_of_countable hα (countable_range f)
+  simpa
+
+protected theorem inter (hα : cof α ≠ ℵ₀) (hs : IsClub s) (ht : IsClub t) : IsClub (s ∩ t) := by
+  simpa [hs, ht] using IsClub.sInter_of_countable (s := {s, t}) hα
 
 theorem _root_.Order.IsNormal.isClub_range {f : α → α} (hf : IsNormal f) : IsClub (.range f) :=
   ⟨hf.dirSupClosed_range, fun x ↦ ⟨_, ⟨x, rfl⟩, hf.strictMono.le_apply⟩⟩
@@ -148,9 +162,32 @@ theorem _root_.Order.IsNormal.isClub_fixedPoints {f : α → α} (hα : cof α 
 theorem ord_cof_eq_isClub_of_isCofinal (hs : IsCofinal s) (hsα : typeLT s = (cof α).ord) :
     ∃ t, s ⊆ t ∧ IsClub t ∧ typeLT t = (cof α).ord := by
   obtain hα | hα := le_or_gt (cof α) ℵ₀
-  · refine ⟨s, subset_rfl, ⟨?_, hs⟩, hsα⟩
-    apply dirSupClosed_of
-  sorry
+  · refine ⟨s, subset_rfl, ⟨dirSupClosed_of_type_le_omega0 hs (hsα.trans_le ?_), hs⟩, hsα⟩
+    simpa using ord_mono hα
+  have : Nonempty α := by
+    by_contra!
+    simp at hα
+  have f : (cof α).ord.ToType ≃o s := (type_lt_eq.1 <| by simp [hsα]).some
+  let g (x : (cof α).ord.ToType) : α :=
+    limitRecOn (motive := fun y ↦ y < (cof α).ord → α) _
+      (fun h ↦ f <| .mk ⟨0, h⟩)
+      (fun y _ hyα ↦ f <| .mk ⟨_, (lt_add_one _).trans hyα⟩)
+      (fun y hy IH hyα ↦ ⨆ z : Iio y, IH _ z.2 (z.2.trans hyα))
+      x.toOrd_lt
+  have hsg : s ⊆ range g := by
+    refine fun x hx ↦ ⟨.mk ⟨f.symm ⟨x, hx⟩ + 1, ?_⟩, ?_⟩
+    · exact (isSuccLimit_ord hα.le).add_one_lt (ToType.toOrd_lt _)
+    · unfold g
+      convert limitRecOn_add_one .. 
+  refine ⟨range g, hsg, ⟨?_, hs.mono hsg⟩, ?_⟩
+  · sorry
+  · conv_rhs => rw [← hsα]
+    apply (type_mono hsg).antisymm'
+    apply (type_range_le _).trans
+    apply le_antisymm <;> rw [type_le_iff']
+    · sorry
+    · refine ⟨⟨embeddingOfSubset _ _ hsg, ?_⟩⟩
+      aesop
 
 variable (α) in
 /-- Every well-order has a club subset of order type `(cof α).ord`. -/
@@ -159,5 +196,136 @@ theorem ord_cof_eq_isClub : ∃ t : Set α, IsClub t ∧ typeLT t = (cof α).ord
   obtain ⟨t, -, ht, ht'⟩ := ord_cof_eq_isClub_of_isCofinal hs hs'
   exact ⟨t, ht, ht'⟩
 
+/-- Every club set has a club subset of order type `(cof α).ord`. -/
+theorem ord_cof_eq_isClub_of_subset (hs : IsClub s) :
+    ∃ t ⊆ s, IsClub t ∧ typeLT t = (cof α).ord := by
+  obtain ⟨t, hts, ht, ht'⟩ := ord_cof_eq_of_isCofinal hs.isCofinal
+  obtain ⟨u, hut, hu, hu'⟩ := ord_cof_eq_isClub_of_isCofinal ht ht'
+  refine ⟨u, ?_, hu, hu'⟩
+  sorry
+
 end WellFoundedLT
 end IsClub
+
+/-! ### Stationary sets -/
+
+/-- A set is called stationary when it intersects all club sets. -/
+@[expose]
+def IsStationary (s : Set α) : Prop :=
+  ∀ ⦃t⦄, IsClub t → (s ∩ t).Nonempty
+
+theorem not_isStationary_iff : ¬ IsStationary s ↔ ∃ t, IsClub t ∧ Disjoint s t := by
+  simp [IsStationary, disjoint_iff, not_nonempty_iff_eq_empty]
+
+@[gcongr]
+theorem IsStationary.mono (hs : IsStationary s) (h : s ⊆ t) : IsStationary t :=
+  fun _u hu ↦ (hs hu).mono (inter_subset_inter_left _ h)
+
+theorem IsStationary.nonempty (hs : IsStationary s) : s.Nonempty := by
+  simpa using hs .univ
+
+theorem isStationary_univ_iff : IsStationary (.univ (α := α)) ↔ Nonempty α := by
+  simp [IsStationary, ← not_imp_not (b := IsClub _), not_nonempty_iff_eq_empty,
+    isClub_empty_iff]
+
+@[simp]
+protected theorem IsStationary.univ [Nonempty α] : IsStationary (.univ (α := α)) :=
+  isStationary_univ_iff.2 ‹_›
+
+@[simp]
+theorem not_isStationary_empty : ¬ IsStationary (∅ : Set α) := by
+  intro h
+  simpa using h .univ
+
+theorem IsClub.isStationary [Nonempty α] [WellFoundedLT α] (hα : cof α ≠ ℵ₀) (hs : IsClub s) :
+    IsStationary s :=
+  fun _ ht ↦ (hs.inter hα ht).nonempty
+
+@[simp]
+theorem not_isStationary_of_isEmpty [IsEmpty α] : ¬ IsStationary s :=
+  s.eq_empty_of_isEmpty ▸ not_isStationary_empty
+
+theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal sᶜ) : IsStationary s := by
+  intro t ht
+  obtain ⟨a, ha⟩ := not_isCofinal_iff.1 hs
+  obtain ⟨b, hb, hb'⟩ := ht.isCofinal a
+  refine ⟨b, ?_, hb⟩
+  contrapose! ha
+  exact ⟨b, ha, hb'⟩
+
+theorem isStationary_iff_not_isCofinal_compl [WellFoundedLT α] (hα : cof α ≤ ℵ₀) :
+    IsStationary s ↔ ¬ IsCofinal (sᶜ) where
+  mp hs h := by
+    obtain ⟨t, hts, ht, htα⟩ := ord_cof_eq_of_isCofinal h
+    have ht' := dirSupClosed_of_type_le_omega0 ht (htα.trans_le ?_)
+    · cases hs ⟨ht', ht⟩
+      grind
+    · simpa using ord_mono hα
+  mpr := .of_not_isCofinal_compl
+
+theorem isStationary_sUnion_iff_of_cof_le_one {s : Set (Set α)} (hα : cof α ≤ 1) :
+    IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x where
+  mp h := by
+    contrapose! h
+    simp_rw [not_isStationary_iff] at h ⊢
+    choose f hf hxf using h
+    refine ⟨⋂ x : s, f _ x.2, ?_, ?_⟩
+    · apply IsClub.iInter_of_cof_le_one hα
+      simpa
+    · rw [disjoint_sUnion_left]
+      exact fun x hx ↦ (hxf _ hx).mono_right (iInter_subset _ ⟨x, hx⟩)
+  mpr := fun ⟨x, hxs, hx⟩ ↦ hx.mono (subset_sUnion_of_mem hxs)
+
+theorem isStationary_iUnion_iff_of_cof_le_one {ι : Type u} {f : ι → Set α} (hα : cof α ≤ 1) :
+    IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i) := by
+  rw [← sUnion_range, isStationary_sUnion_iff_of_cof_le_one hα]
+  simp
+
+theorem isStationary_sUnion_iff_of_orderTop [OrderTop α] {s : Set (Set α)} :
+    IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x :=
+  isStationary_sUnion_iff_of_cof_le_one (by simp)
+
+theorem isStationary_iUnion_iff_of_orderTop [OrderTop α] {ι : Type u} {f : ι → Set α} :
+    IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i) :=
+  isStationary_iUnion_iff_of_cof_le_one (by simp)
+
+section WellFoundedLT
+variable [WellFoundedLT α]
+
+theorem isStationary_sUnion_iff {s : Set (Set α)} (hα : cof α ≠ ℵ₀) (hsα : #s < cof α) :
+    IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x where
+  mp h := by
+    contrapose! h
+    simp_rw [not_isStationary_iff] at h ⊢
+    choose f hf hxf using h
+    refine ⟨⋂ x : s, f _ x.2, ?_, ?_⟩
+    · apply IsClub.iInter hα <;> simpa
+    · rw [disjoint_sUnion_left]
+      exact fun x hx ↦ (hxf _ hx).mono_right (iInter_subset _ ⟨x, hx⟩)
+  mpr := fun ⟨x, hxs, hx⟩ ↦ hx.mono (subset_sUnion_of_mem hxs)
+
+theorem isStationary_iUnion_iff {ι : Type u} {f : ι → Set α} (hα : cof α ≠ ℵ₀)
+    (hι : lift.{v} #ι < lift.{u} (cof α)) : IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i) := by
+  rw [← sUnion_range, isStationary_sUnion_iff hα]
+  · simp
+  · rw [← Cardinal.lift_lt]
+    exact mk_range_le_lift.trans_lt hι
+
+theorem isStationary_sUnion_iff_of_countable {s : Set (Set α)} (hα : cof α ≠ ℵ₀)
+    (hsα : s.Countable) : IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x := by
+  obtain hα | hα := hα.lt_or_gt
+  · apply isStationary_sUnion_iff_of_cof_le_one
+    rwa [← Order.cof_lt_aleph0_iff]
+  · apply isStationary_sUnion_iff hα.ne' (hα.trans_le' _)
+    rwa [le_aleph0_iff_set_countable]
+
+theorem isStationary_iUnion_iff_of_countable {ι : Type*} {f : ι → Set α} [Countable ι]
+    (hα : cof α ≠ ℵ₀) : IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i) := by
+  rw [← sUnion_range, isStationary_sUnion_iff_of_countable hα (countable_range f)]
+  simp
+
+theorem isStationary_union_iff (hα : cof α ≠ ℵ₀) :
+    IsStationary (s ∪ t) ↔ IsStationary s ∨ IsStationary t := by
+  simpa using isStationary_sUnion_iff_of_countable (s := {s, t}) hα
+
+end WellFoundedLT