From 5920dc0d176e25db6b2d61afbf4c2e2a97dd395c Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 5 Apr 2026 11:04:58 -0600 Subject: [PATCH 01/25] more lemmas --- Mathlib/Order/DirSupClosed.lean | 75 +++++++++++++++++++++++++++++---- 1 file changed, 67 insertions(+), 8 deletions(-) diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean index 803eeec2c4672a..30d56cec3faf4c 100644 --- a/Mathlib/Order/DirSupClosed.lean +++ b/Mathlib/Order/DirSupClosed.lean @@ -5,6 +5,7 @@ Authors: Christopher Hoskin, Violeta Hernández Palacios -/ module +public import Mathlib.Order.Antisymmetrization public import Mathlib.Order.CompleteLattice.Defs public import Mathlib.Order.UpperLower.Basic @@ -157,24 +158,82 @@ lemma DirSupInaccOn.union (hs : DirSupInaccOn D s) (ht : DirSupInaccOn D t) : lemma DirSupInacc.union (hs : DirSupInacc s) (ht : DirSupInacc t) : DirSupInacc (s ∪ t) := by simpa using hs.dirSupInaccOn.union ht.dirSupInaccOn (D := .univ) +lemma IsUpperSet.dirSupClosedOn (hs : IsUpperSet s) : DirSupClosedOn D s := + fun _d _ hds ⟨_b, hb⟩ _ _a ha ↦ hs (ha.1 hb) <| hds hb + lemma IsUpperSet.dirSupClosed (hs : IsUpperSet s) : DirSupClosed s := - fun _d hds ⟨_b, hb⟩ _ _a ha ↦ hs (ha.1 hb) <| hds hb + by simpa using hs.dirSupClosedOn (D := univ) + +lemma IsLowerSet.dirSupInaccOn (hs : IsLowerSet s) : DirSupInaccOn D s := + hs.compl.dirSupClosedOn.of_compl + +lemma IsLowerSet.dirSupInacc (hs : IsLowerSet s) : DirSupInacc s := + hs.compl.dirSupClosed.of_compl + +theorem isLUB_congr_of_antisymmRel {a b : α} (h : AntisymmRel (· ≤ ·) a b) : + IsLUB s a ↔ IsLUB s b := by + simp [isLUB_iff_le_iff, h.le_congr_left] + +private theorem DirSupClosed.mem_imp_of_antisymmRel (hs : DirSupClosed s) {a b : α} + (h : AntisymmRel (· ≤ ·) a b) (ha : a ∈ s) : b ∈ s := by + apply hs (singleton_subset_iff.2 ha) ⟨a, rfl⟩ (directedOn_singleton Std.Refl.refl a) + rw [← isLUB_congr_of_antisymmRel h] + exact isLUB_singleton + +theorem DirSupClosed.mem_iff_of_antisymmRel (hs : DirSupClosed s) {a b : α} + (h : AntisymmRel (· ≤ ·) a b) : a ∈ s ↔ b ∈ s := + ⟨hs.mem_imp_of_antisymmRel h, hs.mem_imp_of_antisymmRel h.symm⟩ + +theorem DirSupInacc.mem_iff_of_antisymmRel (hs : DirSupInacc s) {a b : α} + (h : AntisymmRel (· ≤ ·) a b) : a ∈ s ↔ b ∈ s := by + simpa [not_iff_not] using hs.compl.mem_iff_of_antisymmRel h + +lemma dirSupClosedOn_Iic (a : α) : DirSupClosedOn D (Iic a) := + fun _d _ h _ _ _a ha ↦ (isLUB_le_iff ha).2 h -lemma IsLowerSet.dirSupInacc (hs : IsLowerSet s) : DirSupInacc s := hs.compl.dirSupClosed.of_compl +lemma dirSupClosed_Iic (a : α) : DirSupClosed (Iic a) := by + simpa using dirSupClosedOn_Iic a (D := .univ) -lemma dirSupClosed_Iic (a : α) : DirSupClosed (Iic a) := fun _d h _ _ _a ha ↦ (isLUB_le_iff ha).2 h +lemma dirSupInaccOn_Iic (a : α) : DirSupInaccOn D (Iic a) := + (isLowerSet_Iic a).dirSupInaccOn + +lemma dirSupInacc_Iic (a : α) : DirSupInacc (Iic a) := by + simpa using dirSupInaccOn_Iic a (D := .univ) end Preorder +namespace PartialOrder +variable [PartialOrder α] + +theorem dirSupClosedOn_singleton (a : α) : DirSupClosedOn D {a} := by + intro d hD hdu hd₀ hd₁ b hb + rw [subset_singleton_iff_eq] at hdu + obtain rfl | rfl := hdu + · simp at hd₀ + · exact hb.unique isLUB_singleton + +theorem dirSupClosed_singleton (a : α) : DirSupClosed {a} := by + simpa using dirSupClosedOn_singleton a (D := .univ) + +end PartialOrder + section CompleteLattice -variable [CompleteLattice α] {s : Set α} +variable [CompleteLattice α] + +lemma dirSupClosedOn_iff_forall_sSup : DirSupClosedOn D s ↔ + ∀ ⦃d⦄, d ∈ D → d ⊆ s → d.Nonempty → DirectedOn (· ≤ ·) d → sSup d ∈ s := by + simp [DirSupClosedOn, isLUB_iff_sSup_eq] + +lemma dirSupInaccOn_iff_forall_sSup : DirSupInaccOn D s ↔ + ∀ ⦃d⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d → sSup d ∈ s → (d ∩ s).Nonempty := by + simp [DirSupInaccOn, isLUB_iff_sSup_eq] -lemma dirSupClosed_iff_forall_sSup : - DirSupClosed s ↔ ∀ ⦃d⦄, d ⊆ s → d.Nonempty → DirectedOn (· ≤ ·) d → sSup d ∈ s := by +lemma dirSupClosed_iff_forall_sSup : DirSupClosed s ↔ + ∀ ⦃d⦄, d ⊆ s → d.Nonempty → DirectedOn (· ≤ ·) d → sSup d ∈ s := by simp [DirSupClosed, isLUB_iff_sSup_eq] -lemma dirSupInacc_iff_forall_sSup : - DirSupInacc s ↔ ∀ ⦃d⦄, d.Nonempty → DirectedOn (· ≤ ·) d → sSup d ∈ s → (d ∩ s).Nonempty := by +lemma dirSupInacc_iff_forall_sSup : DirSupInacc s ↔ + ∀ ⦃d⦄, d.Nonempty → DirectedOn (· ≤ ·) d → sSup d ∈ s → (d ∩ s).Nonempty := by simp [DirSupInacc, isLUB_iff_sSup_eq] end CompleteLattice From d95fb2dcde005034b56dd8a9ac8da916f47000ae Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 5 Apr 2026 14:29:29 -0600 Subject: [PATCH 02/25] start --- Mathlib/SetTheory/Ordinal/Club.lean | 80 +++++++++++++++++++++++++++++ 1 file changed, 80 insertions(+) create mode 100644 Mathlib/SetTheory/Ordinal/Club.lean diff --git a/Mathlib/SetTheory/Ordinal/Club.lean b/Mathlib/SetTheory/Ordinal/Club.lean new file mode 100644 index 00000000000000..8c140b9677110d --- /dev/null +++ b/Mathlib/SetTheory/Ordinal/Club.lean @@ -0,0 +1,80 @@ +/- +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.SetTheory.Cardinal.Cofinality +public import Mathlib.SetTheory.Ordinal.Family +public import Mathlib.Order.DirSupClosed + +/-! +# 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, 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. +-/ + +@[expose] public section + +universe u + +open Cardinal + +structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where + dirSupClosed : DirSupClosed s + isCofinal : IsCofinal s + +variable {α : Type*} {s t : Set α} {x : α} [LinearOrder α] + +-- This is in another PR. +private theorem DirSupClosed.union (hs : DirSupClosed s) (ht : DirSupClosed t) : + DirSupClosed (s ∪ t) := + sorry + +@[simp] +private theorem DirSupClosed.of_isEmpty [IsEmpty α] (s : Set α) : DirSupClosed s := + fun _ _ ⟨a, _⟩ ↦ isEmptyElim a + +@[simp] +theorem IsClub.of_isEmpty [IsEmpty α] (s : Set α) : IsClub s := + ⟨.of_isEmpty s, .of_isEmpty s⟩ + +theorem IsClub.univ : IsClub (.univ (α := α)) := + ⟨.univ, .univ⟩ + +theorem IsClub.union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) := + ⟨.union hs.dirSupClosed 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₀ (Std.Total.directedOn _) 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₁) + +variable [WellFoundedLT α] + +theorem IsClub.sInter {s : Set (Set α)} (hα : ℵ₀ < Order.cof α) (hsα : #s < Order.cof α) + (hs : ∀ x ∈ s, IsClub x) : IsClub (⋂₀ s) := by + cases isEmpty_or_nonempty α; · simp + have := WellFoundedLT.toOrderBot α + let := WellFoundedLT.conditionallyCompleteLinearOrderBot α + 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)) + sorry + +namespace Ordinal + +protected theorem isClub_sInter {s : Set (Set Ordinal)} [Small.{u} s] (hs : ∀ x ∈ s, IsClub x) : + IsClub (⋂₀ s) := by + refine .sInter ?_ ?_ hs <;> simp From dadb29973575bdb079a49a8a2b784171a0a3937a Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 5 Apr 2026 14:38:21 -0600 Subject: [PATCH 03/25] finish --- Mathlib/SetTheory/Cardinal/Cofinality.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality.lean b/Mathlib/SetTheory/Cardinal/Cofinality.lean index 372d7903291aad..95609eef1e6a3a 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality.lean @@ -725,6 +725,17 @@ theorem cof_univ : cof univ.{u, v} = Cardinal.univ.{u, v} := by ← not_bddAbove_iff_isCofinal] exact fun s hs ↦ mk_le_of_injective (enumOrdOrderIso s hs).injective +@[simp] +theorem _root_.Order.cof_ordinal : Order.cof Ordinal.{u} = Cardinal.univ.{u, u + 1} := by + have := (OrderIso.ofRelIsoLT liftPrincipalSeg.subrelIso.{u, u + 1}).lift_cof_congr + rw [Cardinal.lift_id'.{_, u + 2}] at this + change Order.cof (Iio univ) = _ at this + rwa [cof_Iio, ← lift_cof, Cardinal.lift_inj, cof_univ, eq_comm] at this + +@[simp] +theorem _root_.Order.cof_cardinal : Order.cof Cardinal.{u} = Cardinal.univ.{u, u + 1} := by + rw [← preAleph.cof_congr, cof_ordinal] + end Ordinal namespace Cardinal From fc7d23cf9e6056969518a4e75272c8226eed70c5 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 5 Apr 2026 16:09:53 -0600 Subject: [PATCH 04/25] clubstep --- Mathlib.lean | 1 + Mathlib/Order/DirSupClosed.lean | 16 ++++++ Mathlib/Order/IsNormal.lean | 12 +++++ Mathlib/SetTheory/Ordinal/Basic.lean | 1 + Mathlib/SetTheory/Ordinal/Club.lean | 80 ---------------------------- 5 files changed, 30 insertions(+), 80 deletions(-) delete mode 100644 Mathlib/SetTheory/Ordinal/Club.lean diff --git a/Mathlib.lean b/Mathlib.lean index c21c7fbff44e6e..bc8fbcb0d07dc3 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5753,6 +5753,7 @@ public import Mathlib.Order.Category.Semilat public import Mathlib.Order.Circular public import Mathlib.Order.Circular.ZMod public import Mathlib.Order.Closure +public import Mathlib.Order.Club public import Mathlib.Order.Cofinal public import Mathlib.Order.CompactlyGenerated.Basic public import Mathlib.Order.CompactlyGenerated.Intervals diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean index 803eeec2c4672a..afbbbd91e5771c 100644 --- a/Mathlib/Order/DirSupClosed.lean +++ b/Mathlib/Order/DirSupClosed.lean @@ -62,6 +62,22 @@ 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 := + fun _ _ ⟨a, _⟩ ↦ isEmptyElim a + +@[simp] +theorem DirSupClosedOn.of_isEmpty [IsEmpty α] (s : Set α) : DirSupClosedOn D s := by + simp + +@[simp] +theorem DirSupInacc.of_isEmpty [IsEmpty α] (s : Set α) : DirSupInacc s := + fun _ ⟨a, _⟩ ↦ isEmptyElim a + +@[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 := fun _ a ↦ hf (hD a) diff --git a/Mathlib/Order/IsNormal.lean b/Mathlib/Order/IsNormal.lean index 8e22e8dfd26a91..3438ef95ec78f7 100644 --- a/Mathlib/Order/IsNormal.lean +++ b/Mathlib/Order/IsNormal.lean @@ -5,6 +5,7 @@ Authors: Violeta Hernández Palacios -/ module +public import Mathlib.Dynamics.FixedPoints.Basic public import Mathlib.Order.SuccPred.CompleteLinearOrder public import Mathlib.Order.SuccPred.InitialSeg @@ -130,6 +131,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 diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index 7133072b432cb0..93d13cac260484 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -1317,6 +1317,7 @@ theorem lift_lt_univ' (c : Cardinal) : lift.{max (u + 1) v, u} c < univ.{u, v} : rw [lift_lift, lift_univ, univ_umax.{u, v}] at this exact this +@[simp] theorem aleph0_lt_univ : ℵ₀ < univ.{u, v} := by simpa using lift_lt_univ' ℵ₀ diff --git a/Mathlib/SetTheory/Ordinal/Club.lean b/Mathlib/SetTheory/Ordinal/Club.lean deleted file mode 100644 index 8c140b9677110d..00000000000000 --- a/Mathlib/SetTheory/Ordinal/Club.lean +++ /dev/null @@ -1,80 +0,0 @@ -/- -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.SetTheory.Cardinal.Cofinality -public import Mathlib.SetTheory.Ordinal.Family -public import Mathlib.Order.DirSupClosed - -/-! -# 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, 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. --/ - -@[expose] public section - -universe u - -open Cardinal - -structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where - dirSupClosed : DirSupClosed s - isCofinal : IsCofinal s - -variable {α : Type*} {s t : Set α} {x : α} [LinearOrder α] - --- This is in another PR. -private theorem DirSupClosed.union (hs : DirSupClosed s) (ht : DirSupClosed t) : - DirSupClosed (s ∪ t) := - sorry - -@[simp] -private theorem DirSupClosed.of_isEmpty [IsEmpty α] (s : Set α) : DirSupClosed s := - fun _ _ ⟨a, _⟩ ↦ isEmptyElim a - -@[simp] -theorem IsClub.of_isEmpty [IsEmpty α] (s : Set α) : IsClub s := - ⟨.of_isEmpty s, .of_isEmpty s⟩ - -theorem IsClub.univ : IsClub (.univ (α := α)) := - ⟨.univ, .univ⟩ - -theorem IsClub.union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) := - ⟨.union hs.dirSupClosed 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₀ (Std.Total.directedOn _) 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₁) - -variable [WellFoundedLT α] - -theorem IsClub.sInter {s : Set (Set α)} (hα : ℵ₀ < Order.cof α) (hsα : #s < Order.cof α) - (hs : ∀ x ∈ s, IsClub x) : IsClub (⋂₀ s) := by - cases isEmpty_or_nonempty α; · simp - have := WellFoundedLT.toOrderBot α - let := WellFoundedLT.conditionallyCompleteLinearOrderBot α - 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)) - sorry - -namespace Ordinal - -protected theorem isClub_sInter {s : Set (Set Ordinal)} [Small.{u} s] (hs : ∀ x ∈ s, IsClub x) : - IsClub (⋂₀ s) := by - refine .sInter ?_ ?_ hs <;> simp From d3c8814d589b0e9b781ae820782cd09d656d93b6 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 5 Apr 2026 16:10:04 -0600 Subject: [PATCH 05/25] fix --- Mathlib/Order/Club.lean | 104 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 104 insertions(+) create mode 100644 Mathlib/Order/Club.lean diff --git a/Mathlib/Order/Club.lean b/Mathlib/Order/Club.lean new file mode 100644 index 00000000000000..6105c15d661bb8 --- /dev/null +++ b/Mathlib/Order/Club.lean @@ -0,0 +1,104 @@ +/- +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.SetTheory.Cardinal.Cofinality +public import Mathlib.Order.DirSupClosed + +/-! +# 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. +-/ + +@[expose] public section + +universe u v + +open Cardinal + +/-- 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 s, .of_isEmpty s⟩ + +@[simp] +theorem IsClub.univ : IsClub (.univ (α := α)) := + ⟨.univ, .univ⟩ + +-- Depends on #37304. +proof_wanted IsClub.union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) + +theorem IsClub.isLUB_mem (hs : IsClub s) (ht : t ⊆ s) (ht₀ : t.Nonempty) (hx : IsLUB t x) : x ∈ s := + hs.dirSupClosed ht ht₀ (Std.Total.directedOn _) 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₁) + +variable [WellFoundedLT α] + +attribute [local instance] + WellFoundedLT.toOrderBot WellFoundedLT.conditionallyCompleteLinearOrderBot + +theorem IsClub.sInter {s : Set (Set α)} (hα : ℵ₀ < Order.cof α) (hsα : #s < Order.cof α) + (hs : ∀ x ∈ s, IsClub x) : IsClub (⋂₀ s) := by + cases isEmpty_or_nonempty α; · simp + 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 ↦ (Order.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' ↦ (Order.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α : ℵ₀ < Order.cof α) + (hι : Cardinal.lift.{v} #ι < Cardinal.lift.{u} (Order.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α : ℵ₀ < Order.cof α) (hs : IsClub s) (ht : IsClub t) : + IsClub (s ∩ t) := by + rw [← Set.sInter_pair] + exact IsClub.sInter hα (hα.trans_le' <| by simp) (by simp [hs, ht]) + +theorem Order.IsNormal.isClub_fixedPoints {f : α → α} + (hα : ℵ₀ < Order.cof α) (hf : Order.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'] + · 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 ↦ (Order.cof_le h).not_gt (hα.trans_le' ?_) + simpa using mk_range_le_lift (f := fun n : ℕ ↦ f^[n] a) From 658640cbc0a3c65bc5c5413eca79921c425509c8 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 5 Apr 2026 16:43:05 -0600 Subject: [PATCH 06/25] add of_isEmpty lemmas --- Mathlib/Order/DirSupClosed.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean index 30d56cec3faf4c..f2df8480827d93 100644 --- a/Mathlib/Order/DirSupClosed.lean +++ b/Mathlib/Order/DirSupClosed.lean @@ -63,6 +63,15 @@ 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 := + fun _ _ ⟨a, _⟩ ↦ isEmptyElim a + +@[simp] theorem DirSupInacc.of_isEmpty [IsEmpty α] (s : Set α) : DirSupInacc s := + fun _ ⟨a, _⟩ ↦ isEmptyElim a + +@[simp] theorem DirSupClosedOn.of_isEmpty [IsEmpty α] (s : Set α) : DirSupClosedOn D s := by simp +@[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 := fun _ a ↦ hf (hD a) From a7d780094107055ebaa75d192bf40d351c690cd4 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 5 Apr 2026 16:51:06 -0600 Subject: [PATCH 07/25] simp can prove this --- Mathlib/Order/DirSupClosed.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean index f2df8480827d93..2b1cd15f7f450d 100644 --- a/Mathlib/Order/DirSupClosed.lean +++ b/Mathlib/Order/DirSupClosed.lean @@ -69,8 +69,8 @@ def DirSupInacc (s : Set α) : Prop := @[simp] theorem DirSupInacc.of_isEmpty [IsEmpty α] (s : Set α) : DirSupInacc s := fun _ ⟨a, _⟩ ↦ isEmptyElim a -@[simp] theorem DirSupClosedOn.of_isEmpty [IsEmpty α] (s : Set α) : DirSupClosedOn D s := by simp -@[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 := From cbd1de3dbc45c48339364a4662fad555dba73dc1 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Tue, 21 Apr 2026 19:53:07 -0600 Subject: [PATCH 08/25] move --- Mathlib.lean | 2 +- Mathlib/Order/Club.lean | 104 ---------------------------------------- 2 files changed, 1 insertion(+), 105 deletions(-) delete mode 100644 Mathlib/Order/Club.lean diff --git a/Mathlib.lean b/Mathlib.lean index bc8fbcb0d07dc3..58e6c9ab49a20e 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5753,7 +5753,6 @@ public import Mathlib.Order.Category.Semilat public import Mathlib.Order.Circular public import Mathlib.Order.Circular.ZMod public import Mathlib.Order.Closure -public import Mathlib.Order.Club public import Mathlib.Order.Cofinal public import Mathlib.Order.CompactlyGenerated.Basic public import Mathlib.Order.CompactlyGenerated.Intervals @@ -6846,6 +6845,7 @@ public import Mathlib.RingTheory.ZariskisMainTheorem public import Mathlib.SetTheory.Cardinal.Aleph public import Mathlib.SetTheory.Cardinal.Arithmetic public import Mathlib.SetTheory.Cardinal.Basic +public import Mathlib.SetTheory.Cardinal.Club public import Mathlib.SetTheory.Cardinal.Cofinality public import Mathlib.SetTheory.Cardinal.Continuum public import Mathlib.SetTheory.Cardinal.CountableCover diff --git a/Mathlib/Order/Club.lean b/Mathlib/Order/Club.lean deleted file mode 100644 index 6105c15d661bb8..00000000000000 --- a/Mathlib/Order/Club.lean +++ /dev/null @@ -1,104 +0,0 @@ -/- -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.SetTheory.Cardinal.Cofinality -public import Mathlib.Order.DirSupClosed - -/-! -# 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. --/ - -@[expose] public section - -universe u v - -open Cardinal - -/-- 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 s, .of_isEmpty s⟩ - -@[simp] -theorem IsClub.univ : IsClub (.univ (α := α)) := - ⟨.univ, .univ⟩ - --- Depends on #37304. -proof_wanted IsClub.union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) - -theorem IsClub.isLUB_mem (hs : IsClub s) (ht : t ⊆ s) (ht₀ : t.Nonempty) (hx : IsLUB t x) : x ∈ s := - hs.dirSupClosed ht ht₀ (Std.Total.directedOn _) 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₁) - -variable [WellFoundedLT α] - -attribute [local instance] - WellFoundedLT.toOrderBot WellFoundedLT.conditionallyCompleteLinearOrderBot - -theorem IsClub.sInter {s : Set (Set α)} (hα : ℵ₀ < Order.cof α) (hsα : #s < Order.cof α) - (hs : ∀ x ∈ s, IsClub x) : IsClub (⋂₀ s) := by - cases isEmpty_or_nonempty α; · simp - 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 ↦ (Order.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' ↦ (Order.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α : ℵ₀ < Order.cof α) - (hι : Cardinal.lift.{v} #ι < Cardinal.lift.{u} (Order.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α : ℵ₀ < Order.cof α) (hs : IsClub s) (ht : IsClub t) : - IsClub (s ∩ t) := by - rw [← Set.sInter_pair] - exact IsClub.sInter hα (hα.trans_le' <| by simp) (by simp [hs, ht]) - -theorem Order.IsNormal.isClub_fixedPoints {f : α → α} - (hα : ℵ₀ < Order.cof α) (hf : Order.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'] - · 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 ↦ (Order.cof_le h).not_gt (hα.trans_le' ?_) - simpa using mk_range_le_lift (f := fun n : ℕ ↦ f^[n] a) From 07729e23489b831b6192ea8812a9b62424df6da7 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Tue, 21 Apr 2026 19:56:38 -0600 Subject: [PATCH 09/25] fix --- Mathlib/SetTheory/Cardinal/Club.lean | 104 +++++++++++++++++++++++++++ 1 file changed, 104 insertions(+) create mode 100644 Mathlib/SetTheory/Cardinal/Club.lean diff --git a/Mathlib/SetTheory/Cardinal/Club.lean b/Mathlib/SetTheory/Cardinal/Club.lean new file mode 100644 index 00000000000000..6105c15d661bb8 --- /dev/null +++ b/Mathlib/SetTheory/Cardinal/Club.lean @@ -0,0 +1,104 @@ +/- +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.SetTheory.Cardinal.Cofinality +public import Mathlib.Order.DirSupClosed + +/-! +# 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. +-/ + +@[expose] public section + +universe u v + +open Cardinal + +/-- 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 s, .of_isEmpty s⟩ + +@[simp] +theorem IsClub.univ : IsClub (.univ (α := α)) := + ⟨.univ, .univ⟩ + +-- Depends on #37304. +proof_wanted IsClub.union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) + +theorem IsClub.isLUB_mem (hs : IsClub s) (ht : t ⊆ s) (ht₀ : t.Nonempty) (hx : IsLUB t x) : x ∈ s := + hs.dirSupClosed ht ht₀ (Std.Total.directedOn _) 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₁) + +variable [WellFoundedLT α] + +attribute [local instance] + WellFoundedLT.toOrderBot WellFoundedLT.conditionallyCompleteLinearOrderBot + +theorem IsClub.sInter {s : Set (Set α)} (hα : ℵ₀ < Order.cof α) (hsα : #s < Order.cof α) + (hs : ∀ x ∈ s, IsClub x) : IsClub (⋂₀ s) := by + cases isEmpty_or_nonempty α; · simp + 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 ↦ (Order.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' ↦ (Order.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α : ℵ₀ < Order.cof α) + (hι : Cardinal.lift.{v} #ι < Cardinal.lift.{u} (Order.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α : ℵ₀ < Order.cof α) (hs : IsClub s) (ht : IsClub t) : + IsClub (s ∩ t) := by + rw [← Set.sInter_pair] + exact IsClub.sInter hα (hα.trans_le' <| by simp) (by simp [hs, ht]) + +theorem Order.IsNormal.isClub_fixedPoints {f : α → α} + (hα : ℵ₀ < Order.cof α) (hf : Order.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'] + · 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 ↦ (Order.cof_le h).not_gt (hα.trans_le' ?_) + simpa using mk_range_le_lift (f := fun n : ℕ ↦ f^[n] a) From 0bc5c75bff7036108cbedeb4fd1e57b04ca683e6 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Tue, 21 Apr 2026 19:58:29 -0600 Subject: [PATCH 10/25] rev --- Mathlib/Order/DirSupClosed.lean | 25 +------------------------ 1 file changed, 1 insertion(+), 24 deletions(-) diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean index c1a8e079817582..e66a9411c869f3 100644 --- a/Mathlib/Order/DirSupClosed.lean +++ b/Mathlib/Order/DirSupClosed.lean @@ -167,31 +167,8 @@ lemma DirSupInaccOn.union (hs : DirSupInaccOn D s) (ht : DirSupInaccOn D t) : lemma DirSupInacc.union (hs : DirSupInacc s) (ht : DirSupInacc t) : DirSupInacc (s ∪ t) := by simpa using hs.dirSupInaccOn.union ht.dirSupInaccOn (D := .univ) -lemma IsUpperSet.dirSupClosedOn (hs : IsUpperSet s) : DirSupClosedOn D s := - fun _d _ hds ⟨_b, hb⟩ _ _a ha ↦ hs (ha.1 hb) <| hds hb - lemma IsUpperSet.dirSupClosed (hs : IsUpperSet s) : DirSupClosed s := - by simpa using hs.dirSupClosedOn (D := univ) - -lemma IsLowerSet.dirSupInaccOn (hs : IsLowerSet s) : DirSupInaccOn D s := - hs.compl.dirSupClosedOn.of_compl - -lemma IsLowerSet.dirSupInacc (hs : IsLowerSet s) : DirSupInacc s := - hs.compl.dirSupClosed.of_compl - -theorem isLUB_congr_of_antisymmRel {a b : α} (h : AntisymmRel (· ≤ ·) a b) : - IsLUB s a ↔ IsLUB s b := by - simp [isLUB_iff_le_iff, h.le_congr_left] - -private theorem DirSupClosed.mem_imp_of_antisymmRel (hs : DirSupClosed s) {a b : α} - (h : AntisymmRel (· ≤ ·) a b) (ha : a ∈ s) : b ∈ s := by - apply hs (singleton_subset_iff.2 ha) ⟨a, rfl⟩ (directedOn_singleton Std.Refl.refl a) - rw [← isLUB_congr_of_antisymmRel h] - exact isLUB_singleton - -theorem DirSupClosed.mem_iff_of_antisymmRel (hs : DirSupClosed s) {a b : α} - (h : AntisymmRel (· ≤ ·) a b) : a ∈ s ↔ b ∈ s := - ⟨hs.mem_imp_of_antisymmRel h, hs.mem_imp_of_antisymmRel h.symm⟩ + fun _d hds ⟨_b, hb⟩ _ _a ha ↦ hs (ha.1 hb) <| hds hb lemma IsUpperSet.dirSupClosedOn (hs : IsUpperSet s) : DirSupClosedOn D s := hs.dirSupClosed.dirSupClosedOn From 6c6ea022324f1a3040f493512502f31b5361dd60 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Tue, 21 Apr 2026 20:49:15 -0600 Subject: [PATCH 11/25] generalize thms --- Mathlib/SetTheory/Cardinal/Club.lean | 41 +++++++++++++++++++--- Mathlib/SetTheory/Cardinal/Cofinality.lean | 4 +++ 2 files changed, 41 insertions(+), 4 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Club.lean b/Mathlib/SetTheory/Cardinal/Club.lean index 6105c15d661bb8..228c8f6b8d547e 100644 --- a/Mathlib/SetTheory/Cardinal/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Club.lean @@ -57,14 +57,41 @@ 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α : Order.cof α ≤ 1) + (hs : ∀ x ∈ s, IsClub x) : IsClub (⋂₀ s) := by + cases isEmpty_or_nonempty α; · simp + cases topOrderOrNoTopOrder α + · exact .sInter_of_orderTop hs + · cases (Order.one_lt_cof.trans_le hα).false + +theorem IsClub.iInter_of_cof_le_one {ι : Type*} {f : ι → Set α} (hα : Order.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α : ℵ₀ < Order.cof α) (hsα : #s < Order.cof α) +theorem IsClub.sInter {s : Set (Set α)} (hα : Order.cof α ≠ ℵ₀) (hsα : #s < Order.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 (Order.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)) @@ -80,7 +107,7 @@ theorem IsClub.sInter {s : Set (Set α)} (hα : ℵ₀ < Order.cof α) (hsα : # · exact (hf ⟨t, ht⟩ _).2.trans <| hb ⟨_, rfl⟩ · grind -theorem IsClub.iInter {ι : Type u} {f : ι → Set α} (hα : ℵ₀ < Order.cof α) +theorem IsClub.iInter {ι : Type u} {f : ι → Set α} (hα : Order.cof α ≠ ℵ₀) (hι : Cardinal.lift.{v} #ι < Cardinal.lift.{u} (Order.cof α)) (hf : ∀ i, IsClub (f i)) : IsClub (⋂ i, f i) := by rw [← Set.sInter_range] @@ -88,10 +115,14 @@ theorem IsClub.iInter {ι : Type u} {f : ι → Set α} (hα : ℵ₀ < Order.co rw [← Cardinal.lift_lt] exact mk_range_le_lift.trans_lt hι -theorem IsClub.inter {s t : Set α} (hα : ℵ₀ < Order.cof α) (hs : IsClub s) (ht : IsClub t) : +theorem IsClub.inter {s t : Set α} (hα : Order.cof α ≠ ℵ₀) (hs : IsClub s) (ht : IsClub t) : IsClub (s ∩ t) := by rw [← Set.sInter_pair] - exact IsClub.sInter hα (hα.trans_le' <| by simp) (by simp [hs, ht]) + have H : ∀ x ∈ ({s, t} : Set _), IsClub x := by simpa [hs] + obtain hα | hα' := hα.lt_or_gt + · rw [Order.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_fixedPoints {f : α → α} (hα : ℵ₀ < Order.cof α) (hf : Order.IsNormal f) : IsClub f.fixedPoints := by @@ -102,3 +133,5 @@ theorem Order.IsNormal.isClub_fixedPoints {f : α → α} ⟨_, hf.iSup_iterate_mem_fixedPoints a this, le_csSup this ⟨0, rfl⟩⟩ refine .of_not_isCofinal fun h ↦ (Order.cof_le h).not_gt (hα.trans_le' ?_) simpa using mk_range_le_lift (f := fun n : ℕ ↦ f^[n] a) + +end WellFoundedLT diff --git a/Mathlib/SetTheory/Cardinal/Cofinality.lean b/Mathlib/SetTheory/Cardinal/Cofinality.lean index d071036b42ae89..2e99c56be80df5 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality.lean @@ -163,6 +163,10 @@ 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] +@[simp] +theorem aleph0_le_cof [Nonempty α] [NoMaxOrder α] : ℵ₀ ≤ cof α := by + rw [aleph0_le_cof_iff]; exact one_lt_cof + @[simp] theorem cof_eq_aleph0 [NoMaxOrder α] [Nonempty α] [Countable α] : cof α = ℵ₀ := ((cof_le_cardinalMk _).trans mk_le_aleph0).antisymm (by simp) From aa246e3a0e9949cce41d573e98612c36e17df395 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Tue, 21 Apr 2026 20:49:43 -0600 Subject: [PATCH 12/25] golf --- Mathlib/SetTheory/Cardinal/Club.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Cardinal/Club.lean b/Mathlib/SetTheory/Cardinal/Club.lean index 228c8f6b8d547e..5bd943500135ec 100644 --- a/Mathlib/SetTheory/Cardinal/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Club.lean @@ -73,7 +73,7 @@ theorem IsClub.sInter_of_cof_le_one {s : Set (Set α)} (hα : Order.cof α ≤ 1 cases isEmpty_or_nonempty α; · simp cases topOrderOrNoTopOrder α · exact .sInter_of_orderTop hs - · cases (Order.one_lt_cof.trans_le hα).false + · cases Order.one_lt_cof.not_ge hα theorem IsClub.iInter_of_cof_le_one {ι : Type*} {f : ι → Set α} (hα : Order.cof α ≤ 1) (hs : ∀ i, IsClub (f i)) : IsClub (⋂ i, f i) := by From ead304bfe592d4de8fc3191c19ae7fa13c0b3764 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Tue, 21 Apr 2026 22:00:17 -0600 Subject: [PATCH 13/25] fix --- Mathlib/SetTheory/Cardinal/Cofinality.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality.lean b/Mathlib/SetTheory/Cardinal/Cofinality.lean index 2e99c56be80df5..1440b43042421d 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality.lean @@ -163,9 +163,8 @@ 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] -@[simp] theorem aleph0_le_cof [Nonempty α] [NoMaxOrder α] : ℵ₀ ≤ cof α := by - rw [aleph0_le_cof_iff]; exact one_lt_cof + simp @[simp] theorem cof_eq_aleph0 [NoMaxOrder α] [Nonempty α] [Countable α] : cof α = ℵ₀ := From d472d5c45f05217cd243a09966c6e30faa3ebd01 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Wed, 22 Apr 2026 06:27:03 -0600 Subject: [PATCH 14/25] fix large import --- Mathlib/Order/IsNormal.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Order/IsNormal.lean b/Mathlib/Order/IsNormal.lean index 3438ef95ec78f7..d9c59cae54ea1c 100644 --- a/Mathlib/Order/IsNormal.lean +++ b/Mathlib/Order/IsNormal.lean @@ -5,7 +5,7 @@ Authors: Violeta Hernández Palacios -/ module -public import Mathlib.Dynamics.FixedPoints.Basic +public import Mathlib.Dynamics.FixedPoints.Defs public import Mathlib.Order.SuccPred.CompleteLinearOrder public import Mathlib.Order.SuccPred.InitialSeg From 5400b16f7532c151d8431edeeb5e3b0871f763ea Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 24 Apr 2026 01:45:30 -0600 Subject: [PATCH 15/25] generalize result --- Mathlib/SetTheory/Cardinal/Club.lean | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Club.lean b/Mathlib/SetTheory/Cardinal/Club.lean index 5bd943500135ec..500dd6bc3c7819 100644 --- a/Mathlib/SetTheory/Cardinal/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Club.lean @@ -125,13 +125,18 @@ theorem IsClub.inter {s t : Set α} (hα : Order.cof α ≠ ℵ₀) (hs : IsClub · exact .sInter hα (hα'.trans_le' <| by simp) H theorem Order.IsNormal.isClub_fixedPoints {f : α → α} - (hα : ℵ₀ < Order.cof α) (hf : Order.IsNormal f) : IsClub f.fixedPoints := by + (hα : Order.cof α ≠ ℵ₀) (hf : Order.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'] - · 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 ↦ (Order.cof_le h).not_gt (hα.trans_le' ?_) - simpa using mk_range_le_lift (f := fun n : ℕ ↦ f^[n] a) + · 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 ↦ (Order.cof_le h).not_gt + ((Order.aleph0_le_cof.lt_of_ne' hα).trans_le' ?_) + simpa using mk_range_le_lift (f := fun n : ℕ ↦ f^[n] a) end WellFoundedLT From 5a446de062832fe4b1d129594cbc646985d7b159 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 24 Apr 2026 01:48:05 -0600 Subject: [PATCH 16/25] namespace open --- Mathlib/SetTheory/Cardinal/Club.lean | 32 ++++++++++++++-------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Club.lean b/Mathlib/SetTheory/Cardinal/Club.lean index 500dd6bc3c7819..6fccbee9b20d10 100644 --- a/Mathlib/SetTheory/Cardinal/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Club.lean @@ -26,7 +26,7 @@ topology), `DirSupClosed s` and `IsClosed s` are equivalent predicates. universe u v -open Cardinal +open Cardinal Order /-- A club set is closed under suprema and cofinal. -/ structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where @@ -68,14 +68,14 @@ theorem IsClub.iInter_of_orderTop {ι : Type*} {f : ι → Set α} [OrderTop α] rw [← Set.sInter_range] exact .sInter_of_orderTop (by simpa) -theorem IsClub.sInter_of_cof_le_one {s : Set (Set α)} (hα : Order.cof α ≤ 1) +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 Order.one_lt_cof.not_ge hα + · cases one_lt_cof.not_ge hα -theorem IsClub.iInter_of_cof_le_one {ι : Type*} {f : ι → Set α} (hα : Order.cof α ≤ 1) +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) @@ -87,45 +87,45 @@ variable [WellFoundedLT α] attribute [local instance] WellFoundedLT.toOrderBot WellFoundedLT.conditionallyCompleteLinearOrderBot -theorem IsClub.sInter {s : Set (Set α)} (hα : Order.cof α ≠ ℵ₀) (hsα : #s < Order.cof α) +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 (Order.cof_lt_aleph0_iff.1 hα) hs + · 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 ↦ (Order.cof_le hg).not_gt (hα.trans_le' ?_) + 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' ↦ (Order.cof_le hg').not_gt (mk_range_le.trans_lt hsα) + · 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α : Order.cof α ≠ ℵ₀) - (hι : Cardinal.lift.{v} #ι < Cardinal.lift.{u} (Order.cof α)) (hf : ∀ i, IsClub (f i)) : +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α : Order.cof α ≠ ℵ₀) (hs : IsClub s) (ht : IsClub t) : +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 [Order.cof_lt_aleph0_iff] at hα + · 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_fixedPoints {f : α → α} - (hα : Order.cof α ≠ ℵ₀) (hf : Order.IsNormal f) : IsClub f.fixedPoints := by +theorem 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'] @@ -135,8 +135,8 @@ theorem Order.IsNormal.isClub_fixedPoints {f : α → α} 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 ↦ (Order.cof_le h).not_gt - ((Order.aleph0_le_cof.lt_of_ne' hα).trans_le' ?_) + 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 From f1b46ac8e7b3d529a0260a9398881d3b93f7ca34 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 24 Apr 2026 01:48:52 -0600 Subject: [PATCH 17/25] fix --- Mathlib/SetTheory/Cardinal/Club.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Cardinal/Club.lean b/Mathlib/SetTheory/Cardinal/Club.lean index 6fccbee9b20d10..92f8e938aa9ca9 100644 --- a/Mathlib/SetTheory/Cardinal/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Club.lean @@ -124,7 +124,7 @@ theorem IsClub.inter {s t : Set α} (hα : cof α ≠ ℵ₀) (hs : IsClub s) (h exact .sInter_of_cof_le_one hα H · exact .sInter hα (hα'.trans_le' <| by simp) H -theorem IsNormal.isClub_fixedPoints {f : α → α} (hα : cof α ≠ ℵ₀) (hf : IsNormal f) : +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 ↦ ?_⟩ From 08b5953a4fd3a3a1ec57f94605c378432dd83090 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 1 May 2026 07:52:01 -0600 Subject: [PATCH 18/25] link correct PR --- Mathlib/SetTheory/Cardinal/Club.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Cardinal/Club.lean b/Mathlib/SetTheory/Cardinal/Club.lean index 92f8e938aa9ca9..c330ec1ff10097 100644 --- a/Mathlib/SetTheory/Cardinal/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Club.lean @@ -47,7 +47,7 @@ theorem IsClub.of_isEmpty [IsEmpty α] (s : Set α) : IsClub s := theorem IsClub.univ : IsClub (.univ (α := α)) := ⟨.univ, .univ⟩ --- Depends on #37304. +-- Depends on #38807. proof_wanted IsClub.union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) theorem IsClub.isLUB_mem (hs : IsClub s) (ht : t ⊆ s) (ht₀ : t.Nonempty) (hx : IsLUB t x) : x ∈ s := From 44e2cb5ca00b7437c0085862fc41055ab3f00a3c Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 10 May 2026 15:10:35 -0600 Subject: [PATCH 19/25] union --- .../SetTheory/Cardinal/Cofinality/Club.lean | 142 ++++++++++++++++++ 1 file changed, 142 insertions(+) create mode 100644 Mathlib/SetTheory/Cardinal/Cofinality/Club.lean diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean new file mode 100644 index 00000000000000..8ac9c5f1a782ff --- /dev/null +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -0,0 +1,142 @@ +/- +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.SetTheory.Cardinal.Cofinality.Basic +public import Mathlib.Order.DirSupClosed + +/-! +# 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. +-/ + +@[expose] 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 s, .of_isEmpty s⟩ + +@[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₀ (Std.Total.directedOn _) 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_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 From d65b49e66fdcc60a7cec01ab0449c38d4dbf734e Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 10 May 2026 15:11:02 -0600 Subject: [PATCH 20/25] order imports --- Mathlib/SetTheory/Cardinal/Cofinality/Club.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index 8ac9c5f1a782ff..6d60bfab4026bd 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -5,8 +5,8 @@ Authors: Violeta Hernández Palacios -/ module -public import Mathlib.SetTheory.Cardinal.Cofinality.Basic public import Mathlib.Order.DirSupClosed +public import Mathlib.SetTheory.Cardinal.Cofinality.Basic /-! # Club sets From f594449e5f9dd64c77d212143d108d4cbd9c2ab4 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 10 May 2026 15:12:50 -0600 Subject: [PATCH 21/25] fix import --- Mathlib/SetTheory/Cardinal/Cofinality/Club.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index 6d60bfab4026bd..2479d4120733e9 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -6,6 +6,7 @@ Authors: Violeta Hernández Palacios module public import Mathlib.Order.DirSupClosed +public import Mathlib.Order.IsNormal public import Mathlib.SetTheory.Cardinal.Cofinality.Basic /-! From 9381344c427dbd98baffa2a76b820ef76b8e858e Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 10 May 2026 15:37:52 -0600 Subject: [PATCH 22/25] golf --- Mathlib/SetTheory/Cardinal/Cofinality/Club.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index 2479d4120733e9..98ecd168ec3db0 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -45,7 +45,7 @@ theorem IsClub.of_isEmpty [IsEmpty α] (s : Set α) : IsClub s := ⟨.of_isEmpty s, .of_isEmpty s⟩ @[simp] -theorem IsClub.univ : IsClub (.univ (α := α)) := +theorem IsClub.univ : IsClub (α := α) .univ := ⟨.univ, .univ⟩ theorem IsClub.union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) := From 5229c352b58d4fd75fad4768f1bf308e4e6db86f Mon Sep 17 00:00:00 2001 From: vihdzp Date: Wed, 13 May 2026 04:17:43 -0600 Subject: [PATCH 23/25] implicit --- Mathlib/Order/Cofinal.lean | 4 ++-- Mathlib/Order/DirSupClosed.lean | 8 ++++---- Mathlib/SetTheory/Cardinal/Cofinality/Club.lean | 6 +++--- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/Mathlib/Order/Cofinal.lean b/Mathlib/Order/Cofinal.lean index 9bf81301cea08a..0e8b480d90627f 100644 --- a/Mathlib/Order/Cofinal.lean +++ b/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] diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean index 55a1f0824831de..ead09bf1ac225a 100644 --- a/Mathlib/Order/DirSupClosed.lean +++ b/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 := diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index 98ecd168ec3db0..0b8222270ecde8 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -23,7 +23,7 @@ For any type equipped with the Scott-Hausdorff topology (which includes well-ord topology), `DirSupClosed s` and `IsClosed s` are equivalent predicates. -/ -@[expose] public section +public section universe u v @@ -41,8 +41,8 @@ structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where variable {α : Type v} {s t : Set α} {x : α} [LinearOrder α] @[simp] -theorem IsClub.of_isEmpty [IsEmpty α] (s : Set α) : IsClub s := - ⟨.of_isEmpty s, .of_isEmpty s⟩ +theorem IsClub.of_isEmpty [IsEmpty α] {s : Set α} : IsClub s := + ⟨.of_isEmpty, .of_isEmpty⟩ @[simp] theorem IsClub.univ : IsClub (α := α) .univ := From 9b0ec71b56f3ccf4a5528ffa1f0491df04dddca7 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Wed, 13 May 2026 04:39:40 -0600 Subject: [PATCH 24/25] additions --- Mathlib/SetTheory/Cardinal/Cofinality/Club.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index 0b8222270ecde8..58671ac506a2db 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -52,7 +52,7 @@ 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₀ (Std.Total.directedOn _) hx + 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 := @@ -125,6 +125,9 @@ theorem IsClub.inter {s t : Set α} (hα : cof α ≠ ℵ₀) (hs : IsClub s) (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 From 740c16af535979f0bd31ada4c146c835ba0932c8 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Thu, 14 May 2026 02:33:09 -0600 Subject: [PATCH 25/25] fix --- Mathlib/SetTheory/Ordinal/FixedPoint.lean | 18 ++++++++++++------ .../SetTheory/Ordinal/FundamentalSequence.lean | 2 +- 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/Mathlib/SetTheory/Ordinal/FixedPoint.lean b/Mathlib/SetTheory/Ordinal/FixedPoint.lean index 80b66dc0a5aec2..ce2db50a1c1c51 100644 --- a/Mathlib/SetTheory/Ordinal/FixedPoint.lean +++ b/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]) @@ -396,6 +398,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) @@ -405,15 +408,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] @@ -468,10 +475,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] diff --git a/Mathlib/SetTheory/Ordinal/FundamentalSequence.lean b/Mathlib/SetTheory/Ordinal/FundamentalSequence.lean index 18d98a4fb95d8a..c2247285cf7f62 100644 --- a/Mathlib/SetTheory/Ordinal/FundamentalSequence.lean +++ b/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) :