feat: club sets (#37677)

In set theory, a club set is a subset of an ordinal of uncountable cofinality, which is closed in the order topology, and unbounded within the ordinal.

We generalize this notion to that of a club set in a well-order `α`: this is a set which is cofinal and closed under suprema. We recover the more standard notion by setting `α = Iio o`, whenever `ℵ₀ < o.cof`.

We prove that club sets are closed under intersections of size less than the cofinality of `α`, and that the fixed points of a normal function are a club set.

Author: vihdzp

Mathlib.lean

@@ -6998,6 +6998,7 @@ public import Mathlib.SetTheory.Cardinal.Aleph
 public import Mathlib.SetTheory.Cardinal.Arithmetic
 public import Mathlib.SetTheory.Cardinal.Basic
 public import Mathlib.SetTheory.Cardinal.Cofinality.Basic
+public import Mathlib.SetTheory.Cardinal.Cofinality.Club
 public import Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
 public import Mathlib.SetTheory.Cardinal.Continuum
 public import Mathlib.SetTheory.Cardinal.CountableCover

Mathlib/Order/Cofinal.lean

@@ -34,11 +34,11 @@ variable {α β : Type*}
 section LE
 variable [LE α]
 
-theorem IsCofinal.of_isEmpty [IsEmpty α] (s : Set α) : IsCofinal s :=
+theorem IsCofinal.of_isEmpty [IsEmpty α] {s : Set α} : IsCofinal s :=
   fun a ↦ isEmptyElim a
 
 theorem isCofinal_empty_iff : IsCofinal (∅ : Set α) ↔ IsEmpty α := by
-  refine ⟨fun h ↦ ⟨fun a ↦ ?_⟩, fun h ↦ .of_isEmpty _⟩
+  refine ⟨fun h ↦ ⟨fun a ↦ ?_⟩, fun h ↦ .of_isEmpty⟩
   simpa using h a
 
 @[simp]

Mathlib/Order/DirSupClosed.lean

@@ -63,14 +63,14 @@ def DirSupInacc (s : Set α) : Prop :=
 @[simp] lemma DirSupClosed.dirSupClosedOn : DirSupClosed s → DirSupClosedOn D s := @fun h _ _ ↦ @h _
 @[simp] lemma DirSupInacc.dirSupInaccOn : DirSupInacc s → DirSupInaccOn D s := @fun h _ _ ↦ @h _
 
-@[simp] theorem DirSupClosed.of_isEmpty [IsEmpty α] (s : Set α) : DirSupClosed s :=
+@[simp] theorem DirSupClosed.of_isEmpty [IsEmpty α] {s : Set α} : DirSupClosed s :=
   fun _ _ ⟨a, _⟩ ↦ isEmptyElim a
 
-@[simp] theorem DirSupInacc.of_isEmpty [IsEmpty α] (s : Set α) : DirSupInacc s :=
+@[simp] theorem DirSupInacc.of_isEmpty [IsEmpty α] {s : Set α} : DirSupInacc s :=
   fun _ ⟨a, _⟩ ↦ isEmptyElim a
 
-theorem DirSupClosedOn.of_isEmpty [IsEmpty α] (s : Set α) : DirSupClosedOn D s := by simp
-theorem DirSupInaccOn.of_isEmpty [IsEmpty α] (s : Set α) : DirSupInaccOn D s := by simp
+theorem DirSupClosedOn.of_isEmpty [IsEmpty α] {s : Set α} : DirSupClosedOn D s := by simp
+theorem DirSupInaccOn.of_isEmpty [IsEmpty α] {s : Set α} : DirSupInaccOn D s := by simp
 
 @[gcongr]
 lemma DirSupClosedOn.mono (hD : D₁ ⊆ D₂) (hf : DirSupClosedOn D₂ s) : DirSupClosedOn D₁ s :=

Mathlib/Order/IsNormal.lean

@@ -5,6 +5,7 @@ Authors: Violeta Hernández Palacios
 -/
 module
 
+public import Mathlib.Dynamics.FixedPoints.Defs
 public import Mathlib.Order.DirSupClosed
 public import Mathlib.Order.SuccPred.CompleteLinearOrder
 public import Mathlib.Order.SuccPred.InitialSeg
@@ -131,6 +132,17 @@ theorem map_iSup {ι} [Nonempty ι] {g : ι → α} (hf : IsNormal f) (hg : BddA
   ext
   simp
 
+theorem iSup_iterate_mem_fixedPoints [WellFoundedLT α] {f : α → α} (a : α) (hf : IsNormal f)
+    (hf' : BddAbove (.range fun n ↦ f^[n] a)) : ⨆ n, f^[n] a ∈ f.fixedPoints := by
+  rw [f.mem_fixedPoints_iff, hf.map_iSup hf']
+  apply le_antisymm <;> refine ciSup_le fun n ↦ ?_
+  · rw [← f.iterate_succ_apply']
+    exact le_ciSup hf' _
+  · apply hf.strictMono.le_apply.trans
+    apply (le_ciSup (hf'.mono _) n)
+    simp_rw [← f.iterate_succ_apply']
+    grind
+
 theorem preimage_Iic (hf : IsNormal f) {x : β}
     (h₁ : (f ⁻¹' Iic x).Nonempty) (h₂ : BddAbove (f ⁻¹' Iic x)) :
     f ⁻¹' Iic x = Iic (sSup (f ⁻¹' Iic x)) := by

Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean

@@ -146,6 +146,9 @@ theorem cof_lt_aleph0_iff : Order.cof α < ℵ₀ ↔ Order.cof α ≤ 1 := by
 theorem aleph0_le_cof_iff : ℵ₀ ≤ Order.cof α ↔ 1 < Order.cof α := by
   simp [← not_lt]
 
+theorem aleph0_le_cof [Nonempty α] [NoMaxOrder α] : ℵ₀ ≤ cof α := by
+  simp
+
 @[simp]
 theorem cof_eq_aleph0 [NoMaxOrder α] [Nonempty α] [Countable α] : cof α = ℵ₀ :=
   ((cof_le_cardinalMk _).trans mk_le_aleph0).antisymm (by simp)

Mathlib/SetTheory/Cardinal/Cofinality/Club.lean

@@ -0,0 +1,146 @@
+/-
+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.Order.DirSupClosed
+public import Mathlib.Order.IsNormal
+public import Mathlib.SetTheory.Cardinal.Cofinality.Basic
+
+/-!
+# 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.
+
+## Implementation notes
+
+To avoid importing topology in the ordinals, we spell out the closure property using `DirSupClosed`.
+For any type equipped with the Scott-Hausdorff topology (which includes well-orders with the order
+topology), `DirSupClosed s` and `IsClosed s` are equivalent predicates.
+-/
+
+public section
+
+universe u v
+
+open Cardinal Order
+
+/-- 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
+  condition is equivalent to `IsClosed s`. -/
+  dirSupClosed : DirSupClosed s
+  /-- Club sets are cofinal. If `α` has no maximum, this condition is equivalent to `¬ BddAbove s`.
+  See `not_bddAbove_iff_isCofinal`. -/
+  isCofinal : IsCofinal s
+
+variable {α : Type v} {s t : Set α} {x : α} [LinearOrder α]
+
+@[simp]
+theorem IsClub.of_isEmpty [IsEmpty α] {s : Set α} : IsClub s :=
+  ⟨.of_isEmpty, .of_isEmpty⟩
+
+@[simp]
+theorem IsClub.univ : IsClub (α := α) .univ :=
+  ⟨.univ, .univ⟩
+
+theorem IsClub.union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) :=
+  ⟨hs.dirSupClosed.union ht.dirSupClosed, hs.isCofinal.mono Set.subset_union_left⟩
+
+theorem IsClub.isLUB_mem (hs : IsClub s) (ht : t ⊆ s) (ht₀ : t.Nonempty) (hx : IsLUB t x) : x ∈ s :=
+  hs.dirSupClosed ht ht₀ (.of_linearOrder _) hx
+
+theorem IsClub.csSup_mem {α} [ConditionallyCompleteLinearOrder α] {s t : Set α}
+    (hs : IsClub s) (ht : t ⊆ s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) : sSup t ∈ s :=
+  hs.isLUB_mem ht ht₀ (isLUB_csSup ht₀ ht₁)
+
+theorem IsClub.sInter_of_orderTop {s : Set (Set α)} [OrderTop α]
+    (hs : ∀ x ∈ s, IsClub x) : IsClub (⋂₀ s) := by
+  refine ⟨.sInter fun x hx ↦ (hs x hx).dirSupClosed, ?_⟩
+  rw [isCofinal_iff_top_mem, Set.mem_sInter]
+  exact fun x hx ↦ (hs x hx).isCofinal.top_mem
+
+theorem IsClub.iInter_of_orderTop {ι : Type*} {f : ι → Set α} [OrderTop α]
+    (hs : ∀ i, IsClub (f i)) : IsClub (⋂ i, f i) := by
+  rw [← Set.sInter_range]
+  exact .sInter_of_orderTop (by simpa)
+
+theorem IsClub.sInter_of_cof_le_one {s : Set (Set α)} (hα : cof α ≤ 1)
+    (hs : ∀ x ∈ s, IsClub x) : IsClub (⋂₀ s) := by
+  cases isEmpty_or_nonempty α; · simp
+  cases topOrderOrNoTopOrder α
+  · exact .sInter_of_orderTop hs
+  · cases one_lt_cof.not_ge hα
+
+theorem IsClub.iInter_of_cof_le_one {ι : Type*} {f : ι → Set α} (hα : cof α ≤ 1)
+    (hs : ∀ i, IsClub (f i)) : IsClub (⋂ i, f i) := by
+  rw [← Set.sInter_range]
+  exact .sInter_of_cof_le_one hα (by simpa)
+
+section WellFoundedLT
+
+variable [WellFoundedLT α]
+
+attribute [local instance]
+  WellFoundedLT.toOrderBot WellFoundedLT.conditionallyCompleteLinearOrderBot
+
+theorem IsClub.sInter {s : Set (Set α)} (hα : cof α ≠ ℵ₀) (hsα : #s < cof α)
+    (hs : ∀ x ∈ s, IsClub x) : IsClub (⋂₀ s) := by
+  cases isEmpty_or_nonempty α; · simp
+  obtain hα | hα := hα.lt_or_gt
+  · exact .sInter_of_cof_le_one (cof_lt_aleph0_iff.1 hα) hs
+  refine ⟨.sInter fun x hx ↦ (hs x hx).dirSupClosed, fun a ↦ ?_⟩
+  choose f hf using fun x : s ↦ (hs _ x.2).isCofinal
+  let g : ℕ → α := Nat.rec a fun _ IH ↦ sSup (.range (f · IH))
+  have hg : BddAbove (.range g) := by
+    refine .of_not_isCofinal fun hg ↦ (cof_le hg).not_gt (hα.trans_le' ?_)
+    simpa using mk_range_le_lift (f := g)
+  refine ⟨_, fun t ht ↦ ?_, le_csSup hg ⟨0, rfl⟩⟩
+  apply (hs t ht).isLUB_mem (t := .range fun n ↦ f ⟨t, ht⟩ (g n)) _ (Set.range_nonempty _)
+  · refine ⟨?_, fun b hb ↦ csSup_le' ?_⟩ <;> rintro _ ⟨n, rfl⟩
+    · apply (le_csSup (.of_not_isCofinal _) _).trans (le_csSup hg ⟨n + 1, rfl⟩)
+      · exact fun hg' ↦ (cof_le hg').not_gt (mk_range_le.trans_lt hsα)
+      · use ⟨t, ht⟩
+    · exact (hf ⟨t, ht⟩ _).2.trans <| hb ⟨_, rfl⟩
+  · grind
+
+theorem IsClub.iInter {ι : Type u} {f : ι → Set α} (hα : cof α ≠ ℵ₀)
+    (hι : Cardinal.lift.{v} #ι < Cardinal.lift.{u} (cof α)) (hf : ∀ i, IsClub (f i)) :
+    IsClub (⋂ i, f i) := by
+  rw [← Set.sInter_range]
+  refine IsClub.sInter hα ?_ (by simpa)
+  rw [← Cardinal.lift_lt]
+  exact mk_range_le_lift.trans_lt hι
+
+theorem IsClub.inter {s t : Set α} (hα : cof α ≠ ℵ₀) (hs : IsClub s) (ht : IsClub t) :
+    IsClub (s ∩ t) := by
+  rw [← Set.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 Order.IsNormal.isClub_range {f : α → α} (hf : IsNormal f) : IsClub (.range f) :=
+  ⟨hf.dirSupClosed_range, fun x ↦ ⟨_, ⟨x, rfl⟩, hf.strictMono.le_apply⟩⟩
+
+theorem Order.IsNormal.isClub_fixedPoints {f : α → α} (hα : cof α ≠ ℵ₀) (hf : IsNormal f) :
+    IsClub f.fixedPoints := by
+  cases isEmpty_or_nonempty α; · simp
+  refine ⟨fun s hs hs₀ _ a ha ↦ (hf.map_isLUB ha hs₀).unique ?_, fun a ↦ ?_⟩
+  · rwa [Set.image_congr hs, Set.image_id']
+  · cases topOrderOrNoTopOrder α with
+    | inl => use ⊤; simpa using hf.strictMono.id_le ⊤
+    | inr h =>
+      rw [noTopOrder_iff_noMaxOrder] at h
+      suffices BddAbove (.range fun n ↦ f^[n] a) from
+        ⟨_, hf.iSup_iterate_mem_fixedPoints a this, le_csSup this ⟨0, rfl⟩⟩
+      refine .of_not_isCofinal fun h ↦ (cof_le h).not_gt
+        ((aleph0_le_cof.lt_of_ne' hα).trans_le' ?_)
+      simpa using mk_range_le_lift (f := fun n : ℕ ↦ f^[n] a)
+
+end WellFoundedLT

Mathlib/SetTheory/Ordinal/FixedPoint.lean

@@ -340,6 +340,7 @@ def deriv (f : Ordinal → Ordinal) : Ordinal → Ordinal :=
 theorem deriv_eq_derivFamily (f : Ordinal → Ordinal) : deriv f = derivFamily fun _ : Unit => f :=
   rfl
 
+-- TODO: rename to `deriv_zero` once the name is available
 @[simp]
 theorem deriv_zero_right (f) : deriv f 0 = nfp f 0 :=
   derivFamily_zero _
@@ -361,6 +362,7 @@ theorem isNormal_deriv (f) : IsNormal (deriv f) :=
 theorem deriv_strictMono (f) : StrictMono (deriv f) :=
   derivFamily_strictMono _
 
+@[deprecated "do not depend on the junk values of `nfp`" (since := "2026-05-13")]
 theorem deriv_eq_id_of_nfp_eq_id (h : nfp f = id) : deriv f = id :=
   ((isNormal_deriv _).ext_iff .id).2 (by simp [h])
 
@@ -380,6 +382,7 @@ theorem deriv_eq_enumOrd (H : IsNormal f) : deriv f = enumOrd (Function.fixedPoi
   convert derivFamily_eq_enumOrd fun _ : Unit => H
   exact (Set.iInter_const _).symm
 
+@[deprecated "do not depend on the junk values of `nfp`" (since := "2026-05-13")]
 theorem nfp_zero_left (a) : nfp 0 a = a := by
   rw [← iSup_iterate_eq_nfp]
   apply (Ordinal.iSup_le ?_).antisymm (Ordinal.le_iSup _ 0)
@@ -389,15 +392,19 @@ theorem nfp_zero_left (a) : nfp 0 a = a := by
   · rw [Function.iterate_succ']
     simp
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated "do not depend on the junk values of `nfp`" (since := "2026-05-13")]
 theorem nfp_zero : nfp 0 = id := by
   ext
   exact nfp_zero_left _
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated "do not depend on the junk values of `deriv`" (since := "2026-05-13")]
 theorem deriv_zero : deriv 0 = id :=
   deriv_eq_id_of_nfp_eq_id nfp_zero
 
+set_option linter.deprecated false in
+@[deprecated "do not depend on the junk values of `deriv`" (since := "2026-05-13")]
 theorem deriv_zero_left (a) : deriv 0 a = a := by
   rw [deriv_zero, id_eq]
 
@@ -452,10 +459,9 @@ theorem nfp_mul_zero (a : Ordinal) : nfp (a * ·) 0 = 0 := by
 
 theorem nfp_mul_eq_opow_omega0 {a b : Ordinal} (hb : 0 < b) (hba : b ≤ a ^ ω) :
     nfp (a * ·) b = a ^ ω := by
-  rcases eq_zero_or_pos a with ha | ha
-  · rw [ha, zero_opow omega0_ne_zero] at hba ⊢
-    simp_rw [nonpos_iff_eq_zero.1 hba, zero_mul]
-    exact nfp_zero_left 0
+  rcases eq_zero_or_pos a with rfl | ha
+  · rw [zero_opow omega0_ne_zero] at hba
+    cases hba.not_gt hb
   apply le_antisymm
   · apply nfp_le_fp (isNormal_mul_right ha).monotone hba
     rw [← opow_one_add, one_add_omega0]

Mathlib/SetTheory/Ordinal/FundamentalSequence.lean

@@ -75,7 +75,7 @@ protected theorem id (ho : o ≤ o.cof.ord) : IsFundamentalSeq (o := o) id where
 protected theorem zero (f : Iio 0 → Iio 0) : IsFundamentalSeq f where
   strictMono _ := by simp
   le_ord_cof := by simp
-  isCofinal_range := .of_isEmpty _
+  isCofinal_range := .of_isEmpty
 
 /-- The length one sequence `(o)` is a fundamental sequence for `o + 1`. -/
 protected theorem add_one (o : Ordinal) :