diff --git a/Mathlib.lean b/Mathlib.lean index bcba02b3082cdb..d9dbc6dbd2992b 100644 --- a/Mathlib.lean +++ b/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 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/Order/IsNormal.lean b/Mathlib/Order/IsNormal.lean index e089cb2e7c81ed..df523f0f92b52c 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.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 diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean index 020b1a98d7f2f0..ff288badfea0f4 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean +++ b/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) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean new file mode 100644 index 00000000000000..58671ac506a2db --- /dev/null +++ b/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 diff --git a/Mathlib/SetTheory/Ordinal/FixedPoint.lean b/Mathlib/SetTheory/Ordinal/FixedPoint.lean index cf857d97b41f22..6db8a71ca3c963 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]) @@ -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] 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) :