From 7db31c5fd10b6bb2336392c950d22bc5c9742523 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 5 Apr 2026 14:29:29 -0600 Subject: [PATCH 01/15] 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 b1fdd279ca385392929ed82d9877d45b460e06a0 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 5 Apr 2026 14:38:21 -0600 Subject: [PATCH 02/15] 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 d071036b42ae89..e9453815eeeea3 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality.lean @@ -741,6 +741,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 d03aa864d27d2a02c8ab41f6433806bf4e872db5 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 5 Apr 2026 16:09:53 -0600 Subject: [PATCH 03/15] clubstep --- Mathlib.lean | 1 + Mathlib/Order/DirSupClosed.lean | 16 ++++++ Mathlib/Order/IsNormal.lean | 12 +++++ Mathlib/SetTheory/Ordinal/Club.lean | 80 ----------------------------- 4 files changed, 29 insertions(+), 80 deletions(-) delete mode 100644 Mathlib/SetTheory/Ordinal/Club.lean diff --git a/Mathlib.lean b/Mathlib.lean index 4126812cdba773..620e918d190974 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5778,6 +5778,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/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 cc1d45df26f3c88570aca3a6c582bb7e5f4d435e Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 5 Apr 2026 16:10:04 -0600 Subject: [PATCH 04/15] 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 e9eee7e89abc5939cc1310004b75c3a0bbda39e3 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 5 Apr 2026 11:04:58 -0600 Subject: [PATCH 05/15] 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 afbbbd91e5771c..264f2a491389c2 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 @@ -173,24 +174,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 981b927b3f8fe15a89674cc62e50f401daa5b068 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 5 Apr 2026 21:50:37 -0600 Subject: [PATCH 06/15] fodor --- Mathlib/Order/Club.lean | 123 ++++++++++++++++++++++++++++++++++++++-- 1 file changed, 118 insertions(+), 5 deletions(-) diff --git a/Mathlib/Order/Club.lean b/Mathlib/Order/Club.lean index 6105c15d661bb8..5a7fd55353bf3c 100644 --- a/Mathlib/Order/Club.lean +++ b/Mathlib/Order/Club.lean @@ -9,11 +9,13 @@ public import Mathlib.SetTheory.Cardinal.Cofinality public import Mathlib.Order.DirSupClosed /-! -# Club sets +# Club sets and stationary sets -A subset of a well-ordered type `α` is called a club set when it is closed in the order topology and -cofinal. If `α` has no maximum, then an equivalent condition is that `α` is closed and unbounded; -hence the name. +A subset of a well-ordered type `α` is called a **club set** when it is closed in the order topology +and cofinal. If `α` has no maximum, then an equivalent condition is that `α` is closed and +unbounded; hence the name. + +A set is called **stationary** when it intersects all club sets. ## Implementation notes @@ -26,7 +28,9 @@ topology), `DirSupClosed s` and `IsClosed s` are equivalent predicates. universe u v -open Cardinal +open Cardinal Ordinal + +/-! ### Club sets -/ /-- A club set is closed under suprema and cofinal. -/ structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where @@ -47,6 +51,9 @@ theorem IsClub.of_isEmpty [IsEmpty α] (s : Set α) : IsClub s := theorem IsClub.univ : IsClub (.univ (α := α)) := ⟨.univ, .univ⟩ +theorem isClub_empty_iff : IsClub (α := α) ∅ ↔ IsEmpty α := + ⟨fun h ↦ isCofinal_empty_iff.1 h.isCofinal, fun _ ↦ IsClub.of_isEmpty _⟩ + -- Depends on #37304. proof_wanted IsClub.union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) @@ -57,6 +64,12 @@ 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.ciSup_mem {α} [ConditionallyCompleteLinearOrder α] {ι} {f : ι → α} [Nonempty ι] + {s : Set α} (hs : IsClub s) (ht : .range f ⊆ s) (ht' : BddAbove (.range f)) : ⨆ i, f i ∈ s := + hs.csSup_mem ht (Set.range_nonempty _) ht' + +section WellFoundedLT + variable [WellFoundedLT α] attribute [local instance] @@ -93,6 +106,56 @@ theorem IsClub.inter {s t : Set α} (hα : ℵ₀ < Order.cof α) (hs : IsClub s rw [← Set.sInter_pair] exact IsClub.sInter hα (hα.trans_le' <| by simp) (by simp [hs, ht]) +attribute [-simp] Function.iterate_succ in +/-- Club sets are closed under diagonal intersections. -/ +theorem IsClub.diag {f : α → Set α} (hα' : ℵ₀ < Order.cof α) (hα : typeLT α ≤ (Order.cof α).ord) + (hf : ∀ a, IsClub (f a)) : IsClub {a | ∀ b < a, a ∈ f b} where + dirSupClosed t ht ht₀ _ a ha b hb := by + obtain ⟨c, hc, hbc, -⟩ := ha.exists_between hb + apply (hf b).isLUB_mem _ ⟨c, _⟩ (ha.inter_Ici_of_mem hc) <;> grind + isCofinal a := by + have : Nonempty α := ⟨a⟩ + have := (noTopOrder_iff_noMaxOrder α).1 <| Order.one_lt_cof_iff.1 (one_lt_aleph0.trans hα') + replace hα : (Order.cof α).ord = typeLT α := by + apply hα.antisymm' + rw [ord_le] + exact Order.cof_le_cardinalMk α + have hα'' : Order.cof α = #α := by simpa using congrArg card hα + have (b : α) : ∃ c ∈ ⋂₀ (f '' Set.Iio b), b < c := by + obtain ⟨b', hb'⟩ := exists_gt b + have ⟨c, hc, hbc⟩ := + (IsClub.sInter (s := f '' Set.Iio b) hα' (mk_image_le.trans_lt ?_) ?_).isCofinal b' + · exact ⟨c, hc, hb'.trans_le hbc⟩ + · rw [hα''] + apply mk_Iio_lt + rw [← hα, hα''] + · simp [hf] + choose g hg using this + have hgm : StrictMono fun n ↦ g^[n] a := by + apply strictMono_of_lt_add_one fun n _ ↦ ?_ + rw [← n.succ_eq_add_one, g.iterate_succ_apply'] + exact (hg _).2 + have hg' : IsLUB (.range fun n ↦ g^[n] a) (⨆ n, g^[n] a) := by + refine isLUB_ciSup (.of_not_isCofinal fun h ↦ ?_) + apply (Order.cof_le h).not_gt (hα'.trans_le' _) + simpa using mk_range_le_lift (f := fun n ↦ g^[n] a) + refine ⟨⨆ n, g^[n] a, fun b hb ↦ ?_, hg'.1 ⟨0, rfl⟩⟩ + obtain ⟨_, ⟨n, rfl⟩, hb, hn⟩ := hg'.exists_between hb + apply (hf b).isLUB_mem _ _ (hg'.inter_Ici_of_mem ⟨n + 1, rfl⟩) + · rintro _ ⟨⟨m, rfl⟩, hm⟩ + simp_rw [Set.sInter_image, Set.mem_iInter] at hg + have := (hg (g^[n] a)).1 b hb + cases m with + | zero => + rw [← hm.antisymm (hgm.monotone (zero_le _))] + simpa [← Function.iterate_succ_apply'] using this + | succ m => + dsimp + rw [g.iterate_succ_apply'] + simp_rw [Set.mem_Ici, hgm.le_iff_le, Nat.succ_le_succ_iff] at hm + exact (hg _).1 _ (hb.trans_le <| hgm.monotone hm) + · use g^[n + 1] a; simp + theorem Order.IsNormal.isClub_fixedPoints {f : α → α} (hα : ℵ₀ < Order.cof α) (hf : Order.IsNormal f) : IsClub f.fixedPoints := by cases isEmpty_or_nonempty α; · simp @@ -102,3 +165,53 @@ 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 + +/-! ### Stationary sets -/ + +/-- A set is called stationary when it intersects all club sets. -/ +def IsStationary (s : Set α) : Prop := + ∀ ⦃t⦄, IsClub t → (s ∩ t).Nonempty + +@[gcongr] +theorem IsStationary.mono (hs : IsStationary s) (h : s ⊆ t) : IsStationary t := + fun _u hu ↦ (hs hu).mono (Set.inter_subset_inter_left _ h) + +theorem IsStationary.nonempty (hs : IsStationary s) : s.Nonempty := by + simpa using hs .univ + +theorem isStationary_univ_iff : IsStationary (.univ (α := α)) ↔ Nonempty α := by + simp_rw [IsStationary, Set.univ_inter, ← not_imp_not (b := IsClub _), + Set.not_nonempty_iff_eq_empty, forall_eq, isClub_empty_iff, not_isEmpty_iff] + +@[simp] +theorem IsStationary.univ [Nonempty α] : IsStationary (.univ (α := α)) := + isStationary_univ_iff.2 ‹_› + +theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal (sᶜ)) : IsStationary s := by + rw [not_isCofinal_iff] at hs + intro t ht + obtain ⟨a, ha⟩ := hs + obtain ⟨b, hb, hb'⟩ := ht.isCofinal a + refine ⟨b, ?_, hb⟩ + contrapose! ha + exact ⟨b, ha, hb'⟩ + +proof_wanted isStationary_iff_not_isCofinal_compl (hα : Order.cof α ≤ ℵ₀) : + IsStationary s ↔ ¬ IsCofinal (sᶜ) + +/-- **Fodor's lemma:** if `α` has the order type of a regular cardinal, `s` is a stationary set, and +`f : s → α` is a regressive function, there exists some stationary subset of `s` which is constant +on `f`. -/ +theorem exists_isStationary_preimage_singleton [WellFoundedLT α] {f : s → α} + (hα' : ℵ₀ < Order.cof α) (hα : typeLT α ≤ (Order.cof α).ord) + (hs : IsStationary s) (hf : ∀ x : s, f x < x) : + ∃ a, IsStationary (Subtype.val '' (f ⁻¹' {a})) := by + unfold IsStationary + by_contra! + choose g hg using this + simp_rw [Set.eq_empty_iff_forall_notMem] at hg + obtain ⟨a, hs, ha⟩ := hs <| .diag hα' hα fun a ↦ (hg a).1 + apply (hg (f ⟨a, hs⟩)).2 a + simpa using ⟨hs, ha _ (hf ⟨a, hs⟩)⟩ From 451bcebf5217c7d5e6c06d27e707929fea0ee26f Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 5 Apr 2026 21:52:04 -0600 Subject: [PATCH 07/15] alt name --- Mathlib/Order/Club.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Order/Club.lean b/Mathlib/Order/Club.lean index 5a7fd55353bf3c..3673a6a0438d54 100644 --- a/Mathlib/Order/Club.lean +++ b/Mathlib/Order/Club.lean @@ -201,9 +201,9 @@ theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal (sᶜ)) : IsStati proof_wanted isStationary_iff_not_isCofinal_compl (hα : Order.cof α ≤ ℵ₀) : IsStationary s ↔ ¬ IsCofinal (sᶜ) -/-- **Fodor's lemma:** if `α` has the order type of a regular cardinal, `s` is a stationary set, and -`f : s → α` is a regressive function, there exists some stationary subset of `s` which is constant -on `f`. -/ +/-- **Fodor's lemma,** or the **pressing down lemma:** if `α` has the order type of a regular +cardinal, `s` is a stationary set, and `f : s → α` is a regressive function, there exists some +stationary subset of `s` which is constant on `f`. -/ theorem exists_isStationary_preimage_singleton [WellFoundedLT α] {f : s → α} (hα' : ℵ₀ < Order.cof α) (hα : typeLT α ≤ (Order.cof α).ord) (hs : IsStationary s) (hf : ∀ x : s, f x < x) : From c2342d92caf388d36d1cedb9f9030b8b1fa81b51 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 5 Apr 2026 23:31:09 -0600 Subject: [PATCH 08/15] golf --- Mathlib/Order/Club.lean | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/Mathlib/Order/Club.lean b/Mathlib/Order/Club.lean index 3673a6a0438d54..e10e31e2a62457 100644 --- a/Mathlib/Order/Club.lean +++ b/Mathlib/Order/Club.lean @@ -143,21 +143,19 @@ theorem IsClub.diag {f : α → Set α} (hα' : ℵ₀ < Order.cof α) (hα : ty obtain ⟨_, ⟨n, rfl⟩, hb, hn⟩ := hg'.exists_between hb apply (hf b).isLUB_mem _ _ (hg'.inter_Ici_of_mem ⟨n + 1, rfl⟩) · rintro _ ⟨⟨m, rfl⟩, hm⟩ - simp_rw [Set.sInter_image, Set.mem_iInter] at hg - have := (hg (g^[n] a)).1 b hb + rw [Set.mem_Ici, hgm.le_iff_le, Nat.add_one_le_iff] at hm cases m with - | zero => - rw [← hm.antisymm (hgm.monotone (zero_le _))] - simpa [← Function.iterate_succ_apply'] using this + | zero => contradiction | succ m => dsimp rw [g.iterate_succ_apply'] - simp_rw [Set.mem_Ici, hgm.le_iff_le, Nat.succ_le_succ_iff] at hm + rw [Nat.lt_add_one_iff] at hm + simp_rw [Set.sInter_image, Set.mem_iInter] at hg exact (hg _).1 _ (hb.trans_le <| hgm.monotone hm) · use g^[n + 1] a; simp -theorem Order.IsNormal.isClub_fixedPoints {f : α → α} - (hα : ℵ₀ < Order.cof α) (hf : Order.IsNormal f) : IsClub f.fixedPoints := by +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'] From c89ef364b8587ffec0d1dc45065d2a9bff365f1a Mon Sep 17 00:00:00 2001 From: staroperator Date: Thu, 16 Apr 2026 21:19:12 -0400 Subject: [PATCH 09/15] fix --- Mathlib/Order/DirSupClosed.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean index 264f2a491389c2..34c4693f97578f 100644 --- a/Mathlib/Order/DirSupClosed.lean +++ b/Mathlib/Order/DirSupClosed.lean @@ -192,7 +192,7 @@ theorem isLUB_congr_of_antisymmRel {a b : α} (h : AntisymmRel (· ≤ ·) a b) 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) + apply hs (singleton_subset_iff.2 ha) ⟨a, rfl⟩ (directedOn_singleton a) rw [← isLUB_congr_of_antisymmRel h] exact isLUB_singleton From 3a8c7d005a44e6b58188b86ac4b0cba36d204ff6 Mon Sep 17 00:00:00 2001 From: staroperator Date: Sun, 19 Apr 2026 20:28:17 -0400 Subject: [PATCH 10/15] add --- Mathlib/Order/Bounds/Basic.lean | 4 ++ Mathlib/Order/CompleteLatticeIntervals.lean | 52 +++++++++++++++++++++ Mathlib/Order/LatticeIntervals.lean | 20 ++++++++ 3 files changed, 76 insertions(+) diff --git a/Mathlib/Order/Bounds/Basic.lean b/Mathlib/Order/Bounds/Basic.lean index 4a54c515d9d0f7..63028335d006a9 100644 --- a/Mathlib/Order/Bounds/Basic.lean +++ b/Mathlib/Order/Bounds/Basic.lean @@ -324,6 +324,10 @@ theorem BddAbove.exists_ge [SemilatticeSup γ] {s : Set γ} (hs : BddAbove s) (x theorem isLeast_Ici : IsLeast (Ici a) a := ⟨self_mem_Ici, fun _ => id⟩ +@[to_dual] +theorem isGreatest_Ioi_top [OrderTop α] (ha : ¬ IsMax a) : IsGreatest (Ioi a) ⊤ := + ⟨(not_isMax_iff.1 ha).elim fun _ => lt_top_of_lt, fun _ _ => le_top⟩ + @[to_dual] theorem isLUB_Iic : IsLUB (Iic a) a := isGreatest_Iic.isLUB diff --git a/Mathlib/Order/CompleteLatticeIntervals.lean b/Mathlib/Order/CompleteLatticeIntervals.lean index d55d8efcda1b5b..623c298482c023 100644 --- a/Mathlib/Order/CompleteLatticeIntervals.lean +++ b/Mathlib/Order/CompleteLatticeIntervals.lean @@ -166,6 +166,58 @@ noncomputable instance ordConnectedSubsetConditionallyCompleteLinearOrder [Inhab end OrdConnected +section Iio + +open Classical in +/-- Complete lattice structure on `Set.Iio` -/ +noncomputable instance Set.Iio.conditionallyCompleteLinearOrderBot + [ConditionallyCompleteLinearOrderBot α] {a : α} [Fact (¬ IsMin a)] : + ConditionallyCompleteLinearOrderBot (Iio a) where + __ := (inferInstance : LinearOrder (Iio a)) + __ := orderBot + __ := (inferInstance : Lattice (Iio a)) + sSup S := if hS : BddAbove S then ⟨sSup ((↑) '' S), by + rcases hS with ⟨b, hb⟩ + rw [mem_Iio] + apply b.2.trans_le' + apply csSup_le' + simpa [mem_upperBounds] using hb⟩ else ⊥ + isLUB_csSup S hS hS' := by + simp only [hS', ↓reduceDIte] + refine IsLUB.of_image (f := Subtype.val) (by simp) (isLUB_csSup' ?_) + exact (Subtype.mono_coe _).map_bddAbove hS' + csSup_of_not_bddAbove S hS := by simp [hS] + csSup_empty := by simp + sInf S := if hS : S.Nonempty then ⟨sInf ((↑) '' S), by + rcases hS with ⟨b, hb⟩ + rw [mem_Iio] + apply b.2.trans_le' + apply csInf_le' + simpa using ⟨b.2, hb⟩⟩ else ⊥ + isGLB_csInf S hS hS' := by + simp only [hS, ↓reduceDIte] + refine IsGLB.of_image (f := Subtype.val) (by simp) (isGLB_csInf ?_) + simpa + csInf_of_not_bddBelow := by simp + +lemma Set.Iio.coe_sSup [ConditionallyCompleteLinearOrderBot α] {a : α} [Fact (¬ IsMin a)] + {S : Set (Iio a)} (hS : BddAbove S) : ↑(sSup S) = sSup ((↑) '' S : Set α) := + congrArg Subtype.val (dif_pos hS) + +lemma Set.Iio.coe_sInf [ConditionallyCompleteLinearOrderBot α] {a : α} [Fact (¬ IsMin a)] + {S : Set (Iio a)} (hS : S.Nonempty) : ↑(sInf S) = sInf ((↑) '' S : Set α) := + congrArg Subtype.val (dif_pos hS) + +lemma Set.Iio.coe_iSup [ConditionallyCompleteLinearOrderBot α] {a : α} [Fact (¬ IsMin a)] + {f : ι → Iio a} (hf : BddAbove (range f)) : ↑(iSup f) = (⨆ i, f i : α) := + (coe_sSup hf).trans (congrArg sSup (range_comp Subtype.val f).symm) + +lemma Set.Iio.coe_iInf [ConditionallyCompleteLinearOrderBot α] {a : α} [Fact (¬ IsMin a)] + [Nonempty ι] {f : ι → Iio a} : ↑(iInf f) = (⨅ i, f i : α) := + (coe_sInf (range_nonempty f)).trans (congrArg sInf (range_comp Subtype.val f).symm) + +end Iio + section Icc open Classical in diff --git a/Mathlib/Order/LatticeIntervals.lean b/Mathlib/Order/LatticeIntervals.lean index aa8ec0baffe61d..e1aa9900388cfd 100644 --- a/Mathlib/Order/LatticeIntervals.lean +++ b/Mathlib/Order/LatticeIntervals.lean @@ -67,6 +67,26 @@ protected lemma coe_inf [SemilatticeInf α] {a : α} {x y : Iio a} : ↑(x ⊓ y) = (↑x ⊓ ↑y : α) := rfl +instance semilatticeSup [SemilatticeSup α] [IsLinearOrder α (· ≤ ·)] {a : α} : + SemilatticeSup (Iio a) := + Subtype.semilatticeSup fun x y hx hy => + (Std.Total.total x y).elim (fun h : x ≤ y => by rwa [sup_eq_right.2 h]) fun h => by + rwa [sup_eq_left.2 h] + +@[simp, norm_cast] +protected lemma coe_sup [SemilatticeSup α] [IsLinearOrder α (· ≤ ·)] {a : α} {x y : Iio a} : + ↑(x ⊔ y) = (↑x ⊔ ↑y : α) := + rfl + +instance [Lattice α] [IsLinearOrder α (· ≤ ·)] {a : α} : Lattice (Iio a) where + +instance orderBot [Preorder α] [OrderBot α] {a : α} [Fact (¬ IsMin a)] : OrderBot (Iio a) := + (isLeast_Iio_bot Fact.out).orderBot + +@[simp, norm_cast] +protected lemma coe_bot [Preorder α] [OrderBot α] (a : α) [Fact (¬ IsMin a)] : + (⊥ : Iio a) = (⊥ : α) := rfl + end Iio namespace Ioc From a5a96e47f0bc419c5ffbfbe2110e2bdce950245c Mon Sep 17 00:00:00 2001 From: staroperator Date: Sun, 19 Apr 2026 20:42:44 -0400 Subject: [PATCH 11/15] doc --- Mathlib/Order/CompleteLatticeIntervals.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Order/CompleteLatticeIntervals.lean b/Mathlib/Order/CompleteLatticeIntervals.lean index 623c298482c023..fd9e8c601bbef1 100644 --- a/Mathlib/Order/CompleteLatticeIntervals.lean +++ b/Mathlib/Order/CompleteLatticeIntervals.lean @@ -169,7 +169,7 @@ end OrdConnected section Iio open Classical in -/-- Complete lattice structure on `Set.Iio` -/ +/-- Complete linear order structure on `Set.Iio` -/ noncomputable instance Set.Iio.conditionallyCompleteLinearOrderBot [ConditionallyCompleteLinearOrderBot α] {a : α} [Fact (¬ IsMin a)] : ConditionallyCompleteLinearOrderBot (Iio a) where From 04865bd6257345727ba140844a4c1c0c121bbb11 Mon Sep 17 00:00:00 2001 From: staroperator Date: Sun, 22 Feb 2026 12:51:18 -0500 Subject: [PATCH 12/15] reprove --- Mathlib.lean | 1 + Mathlib/SetTheory/Cardinal/Arithmetic.lean | 39 +++ Mathlib/SetTheory/Cardinal/Basic.lean | 18 ++ Mathlib/SetTheory/Cardinal/DeltaSystem.lean | 313 ++++++++++++++++++++ Mathlib/SetTheory/Cardinal/Pigeonhole.lean | 6 + docs/references.bib | 7 + 6 files changed, 384 insertions(+) create mode 100644 Mathlib/SetTheory/Cardinal/DeltaSystem.lean diff --git a/Mathlib.lean b/Mathlib.lean index 620e918d190974..8318a10440b849 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -6888,6 +6888,7 @@ public import Mathlib.SetTheory.Cardinal.Cofinality public import Mathlib.SetTheory.Cardinal.Continuum public import Mathlib.SetTheory.Cardinal.CountableCover public import Mathlib.SetTheory.Cardinal.Defs +public import Mathlib.SetTheory.Cardinal.DeltaSystem public import Mathlib.SetTheory.Cardinal.Divisibility public import Mathlib.SetTheory.Cardinal.ENat public import Mathlib.SetTheory.Cardinal.Embedding diff --git a/Mathlib/SetTheory/Cardinal/Arithmetic.lean b/Mathlib/SetTheory/Cardinal/Arithmetic.lean index 9a2488ce06242c..0d59bbe0941fe6 100644 --- a/Mathlib/SetTheory/Cardinal/Arithmetic.lean +++ b/Mathlib/SetTheory/Cardinal/Arithmetic.lean @@ -790,6 +790,45 @@ theorem mk_bounded_subset_le {α : Type u} (s : Set α) (c : Cardinal.{u}) : refine (preimage_eq_preimage' ?_ ?_).1 h <;> rw [Subtype.range_coe] <;> assumption rintro ⟨t, _, h2t⟩; exact (mk_preimage_of_injective _ _ Subtype.val_injective).trans h2t +theorem mk_bounded_set_le_powerlt (α : Type u) (c : Cardinal) : + #{t : Set α // #t < c} ≤ c * max #α ℵ₀ ^< c := by + trans #(⋃ i : Set.Iio c.ord, {t : Set α | #t ≤ i.1.card}) + · rw [← coe_setOf] + apply mk_le_mk_of_subset + intro t ht + simp only [Set.mem_setOf, Set.mem_iUnion] at ht ⊢ + exists ⟨(#t).ord, by simpa⟩ + simp + rw [← lift_le.{u + 1}] + apply mk_iUnion_le_sum_mk_lift.trans + apply (sum_le_lift_mk_mul_iSup_lift _).trans + simp only [mk_Iio_ordinal, card_ord, lift_lift, coe_setOf] + rw [← lift_iSup (bddAbove_of_small _), ← lift_mul, lift_le] + apply mul_le_mul_right + rw [powerlt] + refine ciSup_le' fun ⟨i, hi⟩ => ?_ + simp only [mem_Iio, lt_ord] at hi + refine le_ciSup_of_le (bddAbove_of_small _) ⟨i.card, hi⟩ ?_ + apply mk_bounded_set_le + +theorem mk_bounded_subset_le_powerlt {α : Type u} (s : Set α) (c : Cardinal.{u}) : + #{ t : Set α // t ⊆ s ∧ #t < c } ≤ c * max #s ℵ₀ ^< c := by + apply (mk_bounded_set_le_powerlt s c).trans' + refine ⟨Embedding.codRestrict {t : Set s | #t < c} ⟨fun t => (↑) ⁻¹' t.1, ?_⟩ ?_⟩ + · rintro ⟨t, ht1, ht2⟩ ⟨t', h1t', h2t'⟩ h + apply Subtype.ext + dsimp only at h ⊢ + refine (preimage_eq_preimage' ?_ ?_).1 h <;> rw [Subtype.range_coe] <;> assumption + · rintro ⟨t, _, h2t⟩ + exact (mk_preimage_of_injective _ _ Subtype.val_injective).trans_lt h2t + +theorem mk_range_le_powerlt {ι α} {f : ι → Set α} (c : Cardinal.{u}) (s : Set α) + (hf : ∀ i, f i ⊆ s) (hf' : ∀ i, #(f i) < c) : #(Set.range f) ≤ c * max #s ℵ₀ ^< c := by + apply (mk_bounded_subset_le_powerlt s c).trans' + rw [← coe_setOf] + apply mk_le_mk_of_subset + grind + end computing /-! ### Properties of `compl` -/ diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index 387544c2bf75b6..8da8000a8970ee 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -1037,6 +1037,11 @@ theorem powerlt_le_powerlt_left {a b c : Cardinal} (h : b ≤ c) : a ^< b ≤ a theorem powerlt_mono_left (a) : Monotone fun c => a ^< c := fun _ _ => powerlt_le_powerlt_left +theorem powerlt_le_powerlt_right {a b c : Cardinal} (h : a ≤ b) : a ^< c ≤ b ^< c := + powerlt_le.2 fun _ hx => (power_le_power_right h).trans (le_powerlt _ hx) + +theorem powerlt_mono_right (a) : Monotone fun c => c ^< a := fun _ _ => powerlt_le_powerlt_right + theorem powerlt_succ {a b : Cardinal} (h : a ≠ 0) : a ^< succ b = a ^ b := (powerlt_le.2 fun _ h' => power_le_power_left h <| le_of_lt_succ h').antisymm <| le_powerlt a (lt_succ b) @@ -1057,6 +1062,19 @@ theorem powerlt_zero {a : Cardinal} : a ^< 0 = 0 := by convert Cardinal.iSup_of_empty _ exact Subtype.isEmpty_of_false fun x => mem_Iio.not.mpr (Cardinal.zero_le x).not_gt +theorem powerlt_one {a : Cardinal} (h : a ≠ 0) : a ^< 1 = 1 := by + conv_lhs => rw [← succ_zero, powerlt_succ h, power_zero] + +theorem powerlt_eq_zero_iff {a b : Cardinal} : a ^< b = 0 ↔ b = 0 := by + rcases (zero_le b).eq_or_lt with rfl | hb + · simp + rcases (zero_le a).eq_or_lt with rfl | ha + · simp [hb.ne', zero_powerlt hb.ne'] + · simp only [hb.ne', iff_false, ← pos_iff_ne_zero] + rw [← one_le_iff_pos] at hb ⊢ + rw [← powerlt_one ha.ne'] + exact powerlt_le_powerlt_left hb + /-- The cardinality of a set is an upper-bound for the amount of elements before the set's mex (minimum excluded value) -/ theorem _root_.WellFounded.cardinalMk_subtype_lt_min_compl_le {r : α → α → Prop} diff --git a/Mathlib/SetTheory/Cardinal/DeltaSystem.lean b/Mathlib/SetTheory/Cardinal/DeltaSystem.lean new file mode 100644 index 00000000000000..0d979a934440a6 --- /dev/null +++ b/Mathlib/SetTheory/Cardinal/DeltaSystem.lean @@ -0,0 +1,313 @@ +/- +Copyright (c) 2026 Dexin Zhang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Dexin Zhang +-/ +module + +public import Mathlib.SetTheory.Cardinal.Pigeonhole + +/-! +# Δ-systems + +A family of sets forms a Δ-system if they share the same pairwise intersection. This file proves the +Δ-system lemma, which says for any regular cardinal `θ` and infinite cardinal `κ < θ`, if +`∀ c < θ, c ^< κ < θ`, any `θ`-sized family of sets whose cardinalities are less than `κ` must +contain a `θ`-sized Δ-system (this condition is called Δ-system property for `θ` and `κ`, noted as +`Δ(θ, k)`). As a special case, `Δ(ℵ₁, ℵ₀)` ensures any uncountable family of finite sets must +contain an uncountable Δ-system. + +## Main statements + +* `Cardinal.IsRegular.delta_system_property_of_powerlt_lt`: Δ-system lemma for any regular cardinal + `θ` and infinite cardinal `κ < θ`. +* `Cardinal.IsRegular.exists_pairwise_inter_eq_finset` and + `Uncountable.exists_pairwise_inter_eq_finset`: Δ-system lemma specialized for families + of finite sets. + +## TODO + +* Prove that `Δ(θ, κ)` is equivalent to `∀ c < θ, c ^< κ < θ` for any regular cardinal `θ` and + infinite cardinal `κ < θ`. (See .) +* Prove that `Δ(θ, κ)` does not hold for singluar `θ`. + +## References + +* [Kenneth Kunen, *Set Theory: An Introduction to Independence Proofs.*][kunen1980set] +-/ + +@[expose] public section + +universe u v + +namespace Cardinal + +/-- For cardinals `θ` and `κ`, the Δ-system property says any `θ`-sized family of sets whose +cardinalities are less than `κ` must contain a `θ`-sized Δ-system. Also noted as `Δ(θ, κ)`. -/ +def DeltaSystemProperty (θ κ : Cardinal.{u}) := + ∀ ι α (f : ι → Set α), #ι = θ → (∀ i, #(f i) < κ) → + ∃ (s : Set ι) (t : Set α), #s = θ ∧ s.Pairwise (f · ∩ f · = t) + +variable {θ κ : Cardinal.{u}} + +open Order Ordinal Set + +/-- An alternative formalization of Δ-system property, with weaker assumption and stronger +conclusion. -/ +theorem DeltaSystemProperty.exists_pairwise_eq (h : DeltaSystemProperty θ κ) (hκ : 0 < κ) + {ι α : Type u} {f : ι → Set α} (hι : θ ≤ #ι) (hf : ∀ i, #(f i) < κ) : + ∃ (s : Set ι) (t : Set α), #s = θ ∧ #t < κ ∧ s.Pairwise (f · ∩ f · = t) := by + rw [le_mk_iff_exists_set] at hι + rcases hι with ⟨s, hs⟩ + rcases h s α (f ∘ Subtype.val) hs (by grind) with ⟨s', t, hs', ht⟩ + rcases s'.subsingleton_or_nontrivial with hs'' | ⟨x, hx, y, hy, hxy⟩ + · exact ⟨s', ∅, by rwa [mk_image_eq Subtype.val_injective], by simpa, .image <| hs''.pairwise _⟩ + · refine ⟨s', t, by rwa [mk_image_eq Subtype.val_injective], ?_, .image ht⟩ + rw [← ht hx hy hxy] + exact (mk_le_mk_of_subset inter_subset_left).trans_lt (hf _) + +namespace IsRegular + +variable (h : κ < θ) (hκ : ℵ₀ ≤ κ) (hθ : θ.IsRegular) (hθ' : ∀ c < θ, c ^< κ < θ) + +include h hκ hθ hθ' in +private lemma delta_system_property_aux {ι : Type u} {ρ : Ordinal.{u}} {f : ι → Set θ.ord.ToType} + (hι : θ ≤ #ι) (hf : ∀ i, #(f i) < κ) (hρ : ρ < κ.ord) (hρ' : ∀ i, typeLT (f i) = ρ) : + ∃ (s : Set ι) (t : Set θ.ord.ToType), θ ≤ #s ∧ s.Pairwise (f · ∩ f · = t) := by + classical + rcases (zero_le ρ).eq_or_lt with rfl | hρ'' + · simp only [type_eq_zero_iff_isEmpty, isEmpty_coe_sort] at hρ' + exact ⟨Set.univ, ∅, by simpa, by simp [hρ', Set.Pairwise]⟩ + simp_rw [← type_toType ρ, type_eq] at hρ' + have g₁ : ∀ i, ρ.ToType ≃o f i := fun i => OrderIso.ofRelIsoLT (Classical.choice (hρ' i)).symm + haveI : Nonempty θ.ord.ToType := by simpa using ((zero_le κ).trans_lt h).ne' + letI := WellFoundedLT.toOrderBot (α := θ.ord.ToType) + letI := WellFoundedLT.conditionallyCompleteLinearOrderBot θ.ord.ToType + by_cases hξ₀ : ∀ ξ : ρ.ToType, Bounded (· < ·) {(g₁ i ξ).1 | i} + · simp only [Bounded, mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff] at hξ₀ + choose b hb using hξ₀ + have : BddAbove (range b) := by + rw [bddAbove_def] + refine ⟨Ordinal.ToType.mk ⟨⨆ x, (b x).toOrd.1, ?_⟩, ?_⟩ + · rw [mem_Iio] + apply iSup_lt_ord_of_isRegular hθ + · simpa [← lt_ord] using hρ.trans (ord_lt_ord.2 h) + · exact fun i => (b i).toOrd.2 + · simp only [mem_range, forall_exists_index, forall_apply_eq_imp_iff, + ← ToType.mk.symm_apply_le, ← Subtype.coe_le_coe] + exact le_ciSup (Ordinal.bddAbove_of_small _) + let b₀ := iSup b + have : ∀ i, Subtype.val '' range (g₁ i) ⊆ Iio b₀ := by + intro i x hx + simp only [mem_image, mem_range, ↓existsAndEq, true_and] at hx + rcases hx with ⟨x, rfl⟩ + exact (hb _ _).trans_le <| le_ciSup this x + simp_rw [← OrderIso.coe_toEquiv, Equiv.range_eq_univ, image_univ, Subtype.range_val] at this + have : #(range f) < θ := by + apply (mk_range_le_powerlt κ (Iio b₀) this hf).trans_lt + rw [mul_eq_max_of_aleph0_le_left hκ] + · simp only [sup_lt_iff, h, true_and] + apply hθ' + simp only [sup_lt_iff, hκ.trans_lt h, and_true] + exact mk_Iio_ord_toType _ + · simpa [powerlt_eq_zero_iff] using (aleph0_pos.trans_le hκ).ne' + rcases infinite_pigeonhole_card_range f θ hι hθ.aleph0_le (by rwa [hθ.cof_eq]) with ⟨t, ht⟩ + refine ⟨_, t, ht, ?_⟩ + grind [Set.Pairwise] + haveI : Nonempty ρ.ToType := by simpa using hρ''.ne' + letI := Classical.inhabited_of_nonempty (α := ρ.ToType) inferInstance + letI := WellFoundedLT.toOrderBot (α := ρ.ToType) + letI := WellFoundedLT.conditionallyCompleteLinearOrderBot ρ.ToType + let ξ₀ : ρ.ToType := sInf {ξ : ρ.ToType | Unbounded (· < ·) {(g₁ i ξ).1 | (i : ι)}} + replace hξ₀ : Unbounded (· < ·) {(g₁ i ξ₀).1 | i} := by + simp_rw [not_forall, not_bounded_iff] at hξ₀ + apply csInf_mem (s := {ξ | Unbounded (· < ·) {(g₁ i ξ).1 | i}}) + simpa [nonempty_def] + have hξ₀' : ∀ ξ < ξ₀, Bounded (· < ·) {(g₁ i ξ).1 | (i : ι)} := by + intro ξ hξ + apply notMem_of_lt_csInf' at hξ + simpa using hξ + choose! α hα using hξ₀' + simp only [mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff] at hα + let α₀ := ⨆ ξ : Iio ξ₀, α ξ + haveI : NoMaxOrder (θ.ord.ToType) := noMaxOrder hθ.aleph0_le + have hα₀ : ∀ i, ∀ ξ < ξ₀, g₁ i ξ < α₀ := by + intro i ξ hξ + rw [← succ_le_iff] + refine le_ciSup_of_le ?_ ⟨ξ, hξ⟩ ?_ + · refine ⟨Ordinal.ToType.mk ⟨⨆ ξ : Iio ξ₀, α ξ, ?_⟩, ?_⟩ + · rw [mem_Iio] + apply iSup_lt_ord_of_isRegular hθ + · apply (mk_set_le _).trans_lt + apply h.trans' + simpa [← lt_ord] + · exact fun i => (α i).toOrd.2 + · simp only [mem_upperBounds, mem_range, Subtype.exists, mem_Iio, exists_prop, + ← ToType.mk.symm_apply_le, ← Subtype.coe_le_coe, forall_exists_index, and_imp, + forall_apply_eq_imp_iff₂] + intro ξ hξ + exact le_ciSup (Ordinal.bddAbove_range _) (⟨ξ, hξ⟩ : Iio ξ₀) + · rw [succ_le_iff] + exact hα ξ hξ i + haveI : Nonempty ι := by simpa [← mk_ne_zero_iff] using hθ.pos.trans_le hι |>.ne' + let g₂ : θ.ord.ToType → ι := WellFoundedLT.fix fun x ih => + Classical.epsilon fun i => α₀ < g₁ i ξ₀ ∧ ∀ y hy ξ, (g₁ (ih y hy) ξ).1 < g₁ i ξ₀ + have hg₂ : ∀ μ, α₀ < g₁ (g₂ μ) ξ₀ ∧ ∀ ν < μ, ∀ ξ, (g₁ (g₂ ν) ξ).1 < g₁ (g₂ μ) ξ₀ := by + intro μ + suffices ∃ i, α₀ < g₁ i ξ₀ ∧ ∀ ν < μ, ∀ ξ, (g₁ (g₂ ν) ξ).1 < g₁ i ξ₀ by + apply Classical.epsilon_spec at this + unfold g₂ + rwa [WellFoundedLT.fix_eq] + let o : Ordinal := succ (max α₀ (⨆ ν : Iio μ, ⨆ ξ, g₁ (g₂ ν) ξ)) + have ho : o < θ.ord := by + apply (Cardinal.isSuccLimit_ord hθ.aleph0_le).succ_lt + refine max_lt α₀.toOrd.2 ?_ + apply iSup_lt_ord_of_isRegular hθ + · apply mk_Iio_ord_toType + · intro + apply iSup_lt_ord_of_isRegular hθ + · apply h.trans' + simpa [← lt_ord] + · exact fun _ => (Ordinal.ToType.toOrd _).2 + rcases hξ₀ (Ordinal.ToType.mk ⟨o, ho⟩) with ⟨_, ⟨i, rfl⟩, hi⟩ + simp only [not_lt, ← ToType.mk.le_symm_apply, ← Subtype.coe_le_coe, succ_le_iff, sup_lt_iff, + Subtype.coe_lt_coe, OrderIso.lt_iff_lt, o] at hi + rcases hi with ⟨hi₁, hi₂⟩ + refine ⟨i, hi₁, fun ν hν ξ => ?_⟩ + rw [← ToType.mk.symm.lt_iff_lt] + apply hi₂.trans_le' + exact le_ciSup_of_le (Ordinal.bddAbove_range _) ⟨ν, hν⟩ <| + le_ciSup_of_le (Ordinal.bddAbove_range _) ξ le_rfl + have hg₂' : Function.Injective g₂ := by + intro x y h + by_contra! h' + rcases lt_or_gt_of_ne h' with h' | h' + · have := (hg₂ _).2 _ h' ξ₀ + rw [h] at this + simp at this + · have := (hg₂ _).2 _ h' ξ₀ + rw [h] at this + simp at this + have hg₂'' : ∀ x y, x ≠ y → f (g₂ x) ∩ f (g₂ y) ⊆ Iio α₀ := by + intro x y h + wlog h' : x < y generalizing x y + · rw [inter_comm] + exact this _ _ h.symm (lt_of_le_of_ne (le_of_not_gt h') h.symm) + intro z + simp only [mem_inter_iff, mem_Iio, and_imp] + intro hzx hzy + by_contra hz + let ξx := (g₁ (g₂ x)).symm ⟨z, hzx⟩ + let ξy := (g₁ (g₂ y)).symm ⟨z, hzy⟩ + have hξy : ξ₀ ≤ ξy := by + by_contra! + apply hα₀ (g₂ y) at this + simp only [OrderIso.apply_symm_apply, ξy] at this + contradiction + simp only [(g₁ (g₂ y)).le_symm_apply, ← Subtype.coe_le_coe, ξy] at hξy + apply ((hg₂ _).2 _ h' ξx).trans_le at hξy + simp [ξx] at hξy + let g₃ : θ.ord.ToType → Set θ.ord.ToType := fun x => f (g₂ x) ∩ Set.Iio α₀ + have hg₃ : ∀ x, g₃ x ⊆ Set.Iio α₀ := by simp [g₃] + have hg₃' : #(Set.range g₃) < θ := by + refine (mk_range_le_powerlt κ (Iio α₀) hg₃ ?_).trans_lt ?_ + · intro i + refine (mk_le_mk_of_subset ?_).trans_lt (hf (g₂ i)) + grind + · rw [mul_eq_max_of_aleph0_le_left hκ] + · apply max_lt h + apply hθ' + apply max_lt + · exact mk_Iio_ord_toType _ + · exact hκ.trans_lt h + · simp [powerlt_eq_zero_iff, (aleph0_pos.trans_le hκ).ne'] + rcases infinite_pigeonhole_card_range g₃ θ (by rw [mk_ord_toType]) hθ.aleph0_le + (by rwa [hθ.cof_eq]) with ⟨r, hr⟩ + refine ⟨g₂ '' (g₃ ⁻¹' {r}), r, ?_, ?_⟩ + · rwa [mk_image_eq hg₂'] + · apply Pairwise.image + intro x hx y hy hxy + simp only [mem_preimage, mem_singleton_iff, g₃] at hx hy + simpa [← inter_inter_distrib_right, inter_self, inter_eq_left.2 (hg₂'' x y hxy)] + using congr_arg₂ (· ∩ ·) hx hy + +include h hκ hθ hθ' in +/-- **Δ-system lemma**: `Δ(θ, κ)` holds for any regular cardinal `θ` and infinite cardinal `κ < θ` +such that `∀ c < θ, c ^< κ < θ`. -/ +theorem delta_system_property_of_powerlt_lt : DeltaSystemProperty θ κ := by + intro ι α f hι hf + haveI : Nonempty ι := by + simpa [mk_ne_zero_iff] using (aleph0_pos.trans_le hκ |>.trans h |>.trans_le hι.ge).ne' + have : #(⋃ i, f i) ≤ θ := by + refine mk_iUnion_le_sum_mk.trans <| (sum_le_mk_mul_iSup _).trans <| + (mul_le_mul_right (ciSup_mono (bddAbove_of_small _) fun i => (hf i).le) _).trans ?_ + rw [ciSup_const, + mul_eq_left (hκ.trans h.le |>.trans hι.ge) (h.le.trans hι.ge) (aleph0_pos.trans_le hκ).ne', + hι] + rw [← card_ord θ, ← mk_toType, le_def] at this + rcases this with ⟨g⟩ + let g' : ι → Set θ.ord.ToType := fun i => + Set.range ((Set.embeddingOfSubset _ _ (Set.subset_iUnion f i)).trans g) + have hg : ∀ i, #(g' i) < κ := fun i => mk_range_le.trans_lt (hf i) + have hg' : ∀ i, typeLT (g' i) < κ.ord := by simpa [lt_ord, card_type] + rcases infinite_pigeonhole_card (fun i => Ordinal.ToType.mk ⟨typeLT (g' i), hg' i⟩) _ hι.ge + (hκ.trans h.le) (by rwa [mk_ord_toType, hθ.cof_eq]) with ⟨ρ, hs⟩ + generalize hρ : (_ ⁻¹' {ρ}) = s at hs + have : ∃ ρ', ρ = Ordinal.ToType.mk ρ' := ⟨ρ.toOrd, by simp⟩ + rcases this with ⟨⟨ρ, hρ'⟩, rfl⟩ + simp only [mem_Iio] at hρ' + apply (subset_of_eq ∘ Eq.symm) at hρ + simp_rw [subset_def, mem_preimage, mem_singleton_iff, ToType.mk.eq_iff_eq, Subtype.mk_eq_mk] + at hρ + rcases delta_system_property_aux (ι := s) (f := g' ∘ Subtype.val) h hκ hθ hθ' hs (by grind) hρ' + (by grind) with ⟨s', t, hs', ht⟩ + refine ⟨Subtype.val '' s', Subtype.val '' (g ⁻¹' t), ?_, ?_⟩ + · rw [mk_image_eq Subtype.val_injective] + refine hs'.antisymm' <| (mk_set_le _).trans <| (mk_set_le _).trans ?_ + rw [hι] + · refine .image (ht.imp fun x y h => ?_) + simp only [Function.comp_apply] at h + rw [Function.onFun_apply, ← h, preimage_inter, image_inter Subtype.val_injective] + congr <;> ext i <;> simp only [embeddingOfSubset, mem_image, mem_preimage, mem_range, + Function.Embedding.trans_apply, Function.Embedding.coeFn_mk, Subtype.exists, g'] <;> grind + +include hθ in +/-- `Δ(θ, ℵ₀)` holds for any uncountable regular cardinal `θ`. -/ +theorem delta_system_property_aleph0 (hθ' : ℵ₀ < θ) : DeltaSystemProperty θ ℵ₀ := by + apply delta_system_property_of_powerlt_lt hθ' le_rfl hθ + intro c hc + apply (powerlt_aleph0_le _).trans_lt + simp [hc, hθ'] + +include hθ in +/-- **Δ-system lemma** for `Δ(θ, ℵ₀)`: for any uncountable regular cardinal `θ`, any `θ`-sized +family of finite sets must contain a `θ`-sized Δ-system. -/ +theorem exists_pairwise_inter_eq_finset (hθ' : ℵ₀ < θ) {ι : Type u} {α : Type v} [DecidableEq α] + (f : ι → Finset α) (hι : θ ≤ #ι) : + ∃ (s : Set ι) (t : Finset α), #s = θ ∧ s.Pairwise (f · ∩ f · = t) := by + rcases (delta_system_property_aleph0 hθ.lift (aleph0_lt_lift.{u, v}.2 hθ')).exists_pairwise_eq + aleph0_pos (f := fun i : ULift.{v} ι => Equiv.ulift.symm '' (f i.down : Set α)) (by simpa) + (by simp) with ⟨s, t, hs, ht, ht'⟩ + rw [lt_aleph0_iff_subtype_finite, setOf_mem_eq] at ht + refine ⟨Equiv.ulift '' s, Equiv.ulift.finsetCongr ht.toFinset, ?_, ?_⟩ + · rw [← lift_inj.{u, v}, ← lift_umax, mk_image_eq_lift _ _ Equiv.ulift.injective, hs, lift_lift] + · apply Pairwise.image + convert ht' + simp_rw [← Equiv.ulift.finsetCongr.symm_apply_eq] + simp [Finset.map_inter, ← Finset.coe_inj] + +end IsRegular + +end Cardinal + +open Cardinal + +/-- **Δ-system lemma** for `Δ(ℵ₁, ℵ₀)`: any uncountable family of finite sets must contain an +uncountable Δ-system. -/ +theorem Uncountable.exists_pairwise_inter_eq_finset {ι : Type u} {α : Type v} + [Uncountable ι] [DecidableEq α] (f : ι → Finset α) : + ∃ (s : Set ι) (t : Finset α), Uncountable s ∧ s.Pairwise (f · ∩ f · = t) := by + rcases isRegular_aleph_one.exists_pairwise_inter_eq_finset aleph0_lt_aleph_one f + (by simp [← succ_aleph0]) with ⟨s, t, hs, ht⟩ + refine ⟨s, t, ?_, ht⟩ + simpa [← aleph0_lt_mk_iff, hs] using aleph0_lt_aleph_one diff --git a/Mathlib/SetTheory/Cardinal/Pigeonhole.lean b/Mathlib/SetTheory/Cardinal/Pigeonhole.lean index 9917abadfcad1c..6f659198008613 100644 --- a/Mathlib/SetTheory/Cardinal/Pigeonhole.lean +++ b/Mathlib/SetTheory/Cardinal/Pigeonhole.lean @@ -49,6 +49,12 @@ theorem infinite_pigeonhole_card {β α : Type u} (f : β → α) (θ : Cardinal use a; rw [← ha, @preimage_comp _ _ _ Subtype.val f] exact mk_preimage_of_injective _ _ Subtype.val_injective +theorem infinite_pigeonhole_card_range {β α : Type u} (f : β → α) (θ : Cardinal) (hθ : θ ≤ #β) + (h₁ : ℵ₀ ≤ θ) (h₂ : #(Set.range f) < θ.ord.cof) : ∃ a : α, θ ≤ #(f ⁻¹' {a}) := by + rcases infinite_pigeonhole_card (rangeFactorization f) _ hθ h₁ h₂ with ⟨a, ha⟩ + refine ⟨a, ha.trans (mk_le_mk_of_subset ?_)⟩ + grind [rangeFactorization] + theorem infinite_pigeonhole_set {β α : Type u} {s : Set β} (f : s → α) (θ : Cardinal) (hθ : θ ≤ #s) (h₁ : ℵ₀ ≤ θ) (h₂ : #α < θ.ord.cof) : ∃ (a : α) (t : Set β) (h : t ⊆ s), θ ≤ #t ∧ ∀ ⦃x⦄ (hx : x ∈ t), f ⟨x, h hx⟩ = a := by diff --git a/docs/references.bib b/docs/references.bib index 41efdc683252b3..f4ee20d760a0b9 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -3548,6 +3548,13 @@ @Article{ kratschmer_urusov2023 url = {https://doi.org/10.1007/s10959-022-01207-8} } +@Book{ kunen1980set, + title = {Set Theory: An Introduction to Independence Proofs.}, + author = {Kunen, Kenneth}, + year = {1980}, + publisher = {North Holland, Amsterdam} +} + @Book{ kung_rota_yan2009, author = {Kung, Joseph P. S. and Rota, Gian-Carlo and Yan, Catherine H.}, From 88cb94b5f43704c11410224f8e74c9d6aa024291 Mon Sep 17 00:00:00 2001 From: "pre-commit-ci-lite[bot]" <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Date: Sun, 22 Feb 2026 17:53:01 +0000 Subject: [PATCH 13/15] [pre-commit.ci lite] apply automatic fixes --- Mathlib/SetTheory/Cardinal/DeltaSystem.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Cardinal/DeltaSystem.lean b/Mathlib/SetTheory/Cardinal/DeltaSystem.lean index 0d979a934440a6..d60aa0bb977d8a 100644 --- a/Mathlib/SetTheory/Cardinal/DeltaSystem.lean +++ b/Mathlib/SetTheory/Cardinal/DeltaSystem.lean @@ -46,7 +46,7 @@ namespace Cardinal cardinalities are less than `κ` must contain a `θ`-sized Δ-system. Also noted as `Δ(θ, κ)`. -/ def DeltaSystemProperty (θ κ : Cardinal.{u}) := ∀ ι α (f : ι → Set α), #ι = θ → (∀ i, #(f i) < κ) → - ∃ (s : Set ι) (t : Set α), #s = θ ∧ s.Pairwise (f · ∩ f · = t) + ∃ (s : Set ι) (t : Set α), #s = θ ∧ s.Pairwise (f · ∩ f · = t) variable {θ κ : Cardinal.{u}} From 1558ff3230abe1c089b9ea3e469e2015cc3d5caa Mon Sep 17 00:00:00 2001 From: staroperator Date: Thu, 16 Apr 2026 21:19:26 -0400 Subject: [PATCH 14/15] fix --- Mathlib/SetTheory/Cardinal/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index 8da8000a8970ee..e6b817cf42d29a 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -1071,7 +1071,7 @@ theorem powerlt_eq_zero_iff {a b : Cardinal} : a ^< b = 0 ↔ b = 0 := by rcases (zero_le a).eq_or_lt with rfl | ha · simp [hb.ne', zero_powerlt hb.ne'] · simp only [hb.ne', iff_false, ← pos_iff_ne_zero] - rw [← one_le_iff_pos] at hb ⊢ + rw [← Cardinal.one_le_iff_pos] at hb ⊢ rw [← powerlt_one ha.ne'] exact powerlt_le_powerlt_left hb From e969f2c83b1e90e09dc085979658ea8f76e5bc5e Mon Sep 17 00:00:00 2001 From: staroperator Date: Sun, 19 Apr 2026 21:29:36 -0400 Subject: [PATCH 15/15] reprove --- Mathlib/Order/Club.lean | 117 ++++++- Mathlib/Order/DirSupClosed.lean | 8 + Mathlib/SetTheory/Cardinal/Arithmetic.lean | 4 +- Mathlib/SetTheory/Cardinal/Basic.lean | 17 ++ Mathlib/SetTheory/Cardinal/Cofinality.lean | 28 ++ Mathlib/SetTheory/Cardinal/DeltaSystem.lean | 323 +++++++------------- Mathlib/SetTheory/Ordinal/Arithmetic.lean | 3 + Mathlib/SetTheory/Ordinal/Basic.lean | 10 + docs/references.bib | 7 + 9 files changed, 309 insertions(+), 208 deletions(-) diff --git a/Mathlib/Order/Club.lean b/Mathlib/Order/Club.lean index e10e31e2a62457..678ccffba70f92 100644 --- a/Mathlib/Order/Club.lean +++ b/Mathlib/Order/Club.lean @@ -5,9 +5,12 @@ Authors: Violeta Hernández Palacios -/ module -public import Mathlib.SetTheory.Cardinal.Cofinality +public import Mathlib.SetTheory.Cardinal.Regular public import Mathlib.Order.DirSupClosed +import Mathlib.Data.Set.Monotone +import Mathlib.Order.CompleteLatticeIntervals + /-! # Club sets and stationary sets @@ -54,6 +57,10 @@ theorem IsClub.univ : IsClub (.univ (α := α)) := theorem isClub_empty_iff : IsClub (α := α) ∅ ↔ IsEmpty α := ⟨fun h ↦ isCofinal_empty_iff.1 h.isCofinal, fun _ ↦ IsClub.of_isEmpty _⟩ +theorem IsClub.nonempty [Nonempty α] (hs : IsClub s) : s.Nonempty := by + by_contra! + simp [isClub_empty_iff, this] at hs + -- Depends on #37304. proof_wanted IsClub.union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) @@ -68,6 +75,10 @@ theorem IsClub.ciSup_mem {α} [ConditionallyCompleteLinearOrder α] {ι} {f : ι {s : Set α} (hs : IsClub s) (ht : .range f ⊆ s) (ht' : BddAbove (.range f)) : ⨆ i, f i ∈ s := hs.csSup_mem ht (Set.range_nonempty _) ht' +theorem isClub_Ioi [NoMaxOrder α] (x : α) : IsClub (Set.Ioi x) where + dirSupClosed := dirSupClosed_Ioi x + isCofinal := .of_not_bddAbove (not_bddAbove_Ioi x) + section WellFoundedLT variable [WellFoundedLT α] @@ -101,6 +112,12 @@ theorem IsClub.iInter {ι : Type u} {f : ι → Set α} (hα : ℵ₀ < Order.co rw [← Cardinal.lift_lt] exact mk_range_le_lift.trans_lt hι +theorem IsClub.biInter {ι : Type u} {s : Set ι} {f : ι → Set α} (hα : ℵ₀ < Order.cof α) + (hs : Cardinal.lift.{v} #s < Cardinal.lift.{u} (Order.cof α)) (hf : ∀ i ∈ s, IsClub (f i)) : + IsClub (⋂ i ∈ s, f i) := by + rw [Set.biInter_eq_iInter] + exact iInter hα hs (by simpa) + theorem IsClub.inter {s t : Set α} (hα : ℵ₀ < Order.cof α) (hs : IsClub s) (ht : IsClub t) : IsClub (s ∩ t) := by rw [← Set.sInter_pair] @@ -164,6 +181,10 @@ theorem Order.IsNormal.isClub_fixedPoints {f : α → α} (hα : ℵ₀ < cof α 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) +lemma isClub_almost_fixed_points [NoMaxOrder α] {f : α → α} (hα' : ℵ₀ < Order.cof α) + (hα : typeLT α ≤ (Order.cof α).ord) : IsClub {x : α | ∀ y < x, f y < x} := + IsClub.diag hα' hα fun x => isClub_Ioi (f x) + end WellFoundedLT /-! ### Stationary sets -/ @@ -187,6 +208,11 @@ theorem isStationary_univ_iff : IsStationary (.univ (α := α)) ↔ Nonempty α theorem IsStationary.univ [Nonempty α] : IsStationary (.univ (α := α)) := isStationary_univ_iff.2 ‹_› +theorem IsStationary.not_bddAbove [NoMaxOrder α] (hs : IsStationary s) : ¬ BddAbove s := by + by_contra ⟨a, ha⟩ + apply (hs (isClub_Ioi a)).ne_empty + simpa [Set.eq_empty_iff_forall_notMem, mem_upperBounds] using ha + theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal (sᶜ)) : IsStationary s := by rw [not_isCofinal_iff] at hs intro t ht @@ -199,6 +225,12 @@ theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal (sᶜ)) : IsStati proof_wanted isStationary_iff_not_isCofinal_compl (hα : Order.cof α ≤ ℵ₀) : IsStationary s ↔ ¬ IsCofinal (sᶜ) +theorem IsStationary.inter_isClub [WellFoundedLT α] (hα : ℵ₀ < Order.cof α) (hs : IsStationary s) + (ht : IsClub t) : IsStationary (s ∩ t) := by + intro t' ht' + rw [Set.inter_assoc] + exact hs (ht.inter hα ht') + /-- **Fodor's lemma,** or the **pressing down lemma:** if `α` has the order type of a regular cardinal, `s` is a stationary set, and `f : s → α` is a regressive function, there exists some stationary subset of `s` which is constant on `f`. -/ @@ -213,3 +245,86 @@ theorem exists_isStationary_preimage_singleton [WellFoundedLT α] {f : s → α} obtain ⟨a, hs, ha⟩ := hs <| .diag hα' hα fun a ↦ (hg a).1 apply (hg (f ⟨a, hs⟩)).2 a simpa using ⟨hs, ha _ (hf ⟨a, hs⟩)⟩ + +lemma exists_isStationary_preimage_singleton_of_cardinalMk_range_lt_cof [WellFoundedLT α] + {f : s → Set α} (hα : ℵ₀ < Order.cof α) (hs : IsStationary s) + (hf : #(Set.range f) < Order.cof α) : ∃ a, IsStationary (Subtype.val '' (f ⁻¹' {a})) := by + unfold IsStationary + by_contra! + choose g hg using this + apply (hs (.biInter hα (by simpa) fun i _ => (hg i).1)).ne_empty + rw [Set.eq_empty_iff_forall_notMem] + intro x hx + rw [Set.mem_inter_iff, Set.mem_iInter₂] at hx + apply Set.not_nonempty_iff_eq_empty.2 (hg (f ⟨x, hx.1⟩)).2 + exists x + grind [Subtype.exists] + +/-- For regular cardinals `α < κ`, the set `{o < κ | cof o = α}` is stationary in `κ`. -/ +lemma Cardinal.IsRegular.isStationary_setOf_cof_eq {α κ : Cardinal.{u}} (hκ : κ.IsRegular) + (hα : α.IsRegular) (h : α < κ) : IsStationary {o : Set.Iio κ.ord | cof o = α} := by + intro C hC + haveI : NoMaxOrder (Set.Iio κ.ord) := noMaxOrder_Iio_ord hκ.aleph0_le + haveI : Fact (¬ IsMin κ.ord) := ⟨by simp [pos_iff_ne_zero.1 hκ.pos]⟩ + rcases hC.nonempty with ⟨a, ha⟩ + have := not_bddAbove_iff_isCofinal.2 hC.isCofinal + simp only [bddAbove_def, not_exists, not_forall, exists_prop, not_le] at this + choose! f hf₁ hf₂ using this + let g : Ordinal.{u} → Set.Iio κ.ord := fun x => + Ordinal.limitRecOn x a (fun _ => f) fun x _ ih => ⨆ y : Set.Iio x, ih y.1 y.2 + have hg0 : g 0 = a := by simp [g] + have hg_succ : ∀ x, g (Order.succ x) = f (g x) := by simp [g, -Order.succ_eq_add_one] + have hg_limit : ∀ x, Order.IsSuccLimit x → g x = ⨆ y : Set.Iio x, g y := by + simp +contextual [g, Ordinal.limitRecOn_limit] + have hg₁ : ∀ x < κ.ord, g x ∈ C := by + intro x hx + induction x using Ordinal.limitRecOn with + | zero => simpa [hg0] + | succ x ih => + grind [Order.lt_succ] + | limit x hx' ih => + simp only [hx', hg_limit] + haveI : Nonempty (Set.Iio x) := ⟨0, by simpa using hx'.bot_lt⟩ + apply hC.ciSup_mem + · grind + · apply bddAbove_range_Iio_of_lt_cof + rwa [hκ.cof_ord, mk_Iio_ordinal, lift_lift, lift_lt, ← lt_ord] + have hg₂ : StrictMonoOn g (Set.Iio κ.ord) := by + intro x hx y hy h + simp only [Set.mem_Iio] at hx hy + induction y using Ordinal.limitRecOn generalizing x with + | zero => simp at h + | succ y ih => + simp only [hg_succ] + apply (hf₂ _).trans_le' + rw [Order.lt_succ_iff, le_iff_lt_or_eq] at h + grind [Order.lt_succ] + | limit y hy' ih => + simp only [hy', hg_limit] + apply (hf₂ _).trans_le + rw [← hg_succ] + refine le_ciSup_of_le ?_ (⟨Order.succ x, ?_⟩ : Set.Iio y) le_rfl + · apply bddAbove_range_Iio_of_lt_cof + rwa [hκ.cof_ord, mk_Iio_ordinal, lift_lift, lift_lt, ← lt_ord] + · simpa [-Order.succ_eq_add_one] using hy'.succ_lt h + simp only [Set.nonempty_def, Set.mem_inter_iff, Set.mem_setOf_eq] + refine ⟨g α.ord, ?_, ?_⟩ + · rw [hg_limit _ (Cardinal.isSuccLimit_ord hα.aleph0_le), + Set.Iio.coe_iSup (bddAbove_range_Iio_of_lt_cof (by simpa [hκ.cof_ord])), + Ordinal.cof_iSup_Iio, hα.cof_ord] + · exact (hg₂.mono (Set.Iio_subset_Iio (Cardinal.ord_le_ord.2 h.le))).strictMono + · exact (Cardinal.isSuccLimit_ord hα.aleph0_le).isSuccPrelimit + · grind [Cardinal.ord_lt_ord] + +lemma Cardinal.IsRegular.card_eq_of_isStationary {c : Cardinal.{u}} (hc : c.IsRegular) + {s : Set (Set.Iio c.ord)} (hs : IsStationary s) : #s = Cardinal.lift.{u + 1} c := by + apply le_antisymm + · grw [mk_set_le] + simp + conv_lhs => rw [← hc.cof_ord, lift_cof, ← cof_Iio] + by_contra! h + haveI : NoMaxOrder (Set.Iio c.ord) := noMaxOrder_Iio_ord hc.aleph0_le + apply hs.not_bddAbove + contrapose! h + rw [not_bddAbove_iff_isCofinal] at h + exact Order.cof_le h diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean index 34c4693f97578f..74c6d1736e83f4 100644 --- a/Mathlib/Order/DirSupClosed.lean +++ b/Mathlib/Order/DirSupClosed.lean @@ -210,6 +210,14 @@ lemma dirSupClosedOn_Iic (a : α) : DirSupClosedOn D (Iic a) := lemma dirSupClosed_Iic (a : α) : DirSupClosed (Iic a) := by simpa using dirSupClosedOn_Iic a (D := .univ) +lemma dirSupClosedOn_Ioi (a : α) : DirSupClosedOn D (Ioi a) := by + intro s _ hs hs' _ b hb + rcases hs' with ⟨c, hc⟩ + exact (hs hc).trans_le (hb.1 hc) + +lemma dirSupClosed_Ioi (a : α) : DirSupClosed (Ioi a) := by + simpa using dirSupClosedOn_Ioi a (D := .univ) + lemma dirSupInaccOn_Iic (a : α) : DirSupInaccOn D (Iic a) := (isLowerSet_Iic a).dirSupInaccOn diff --git a/Mathlib/SetTheory/Cardinal/Arithmetic.lean b/Mathlib/SetTheory/Cardinal/Arithmetic.lean index 0d59bbe0941fe6..e5d7cacc7dc335 100644 --- a/Mathlib/SetTheory/Cardinal/Arithmetic.lean +++ b/Mathlib/SetTheory/Cardinal/Arithmetic.lean @@ -803,12 +803,12 @@ theorem mk_bounded_set_le_powerlt (α : Type u) (c : Cardinal) : apply mk_iUnion_le_sum_mk_lift.trans apply (sum_le_lift_mk_mul_iSup_lift _).trans simp only [mk_Iio_ordinal, card_ord, lift_lift, coe_setOf] - rw [← lift_iSup (bddAbove_of_small _), ← lift_mul, lift_le] + rw [← lift_iSup bddAbove_of_small, ← lift_mul, lift_le] apply mul_le_mul_right rw [powerlt] refine ciSup_le' fun ⟨i, hi⟩ => ?_ simp only [mem_Iio, lt_ord] at hi - refine le_ciSup_of_le (bddAbove_of_small _) ⟨i.card, hi⟩ ?_ + refine le_ciSup_of_le bddAbove_of_small ⟨i.card, hi⟩ ?_ apply mk_bounded_set_le theorem mk_bounded_subset_le_powerlt {α : Type u} (s : Set α) (c : Cardinal.{u}) : diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean index e6b817cf42d29a..f939509dbdce4f 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -1042,6 +1042,10 @@ theorem powerlt_le_powerlt_right {a b c : Cardinal} (h : a ≤ b) : a ^< c ≤ b theorem powerlt_mono_right (a) : Monotone fun c => c ^< a := fun _ _ => powerlt_le_powerlt_right +@[gcongr] +theorem powerlt_le_powerlt {a b c d : Cardinal} (h₁ : a ≤ b) (h₂ : c ≤ d) : a ^< c ≤ b ^< d := + (powerlt_le_powerlt_right h₁).trans (powerlt_le_powerlt_left h₂) + theorem powerlt_succ {a b : Cardinal} (h : a ≠ 0) : a ^< succ b = a ^ b := (powerlt_le.2 fun _ h' => power_le_power_left h <| le_of_lt_succ h').antisymm <| le_powerlt a (lt_succ b) @@ -1075,6 +1079,19 @@ theorem powerlt_eq_zero_iff {a b : Cardinal} : a ^< b = 0 ↔ b = 0 := by rw [← powerlt_one ha.ne'] exact powerlt_le_powerlt_left hb +@[simp] +theorem lift_powerlt (a b : Cardinal.{u}) : lift.{v} (a ^< b) = lift.{v} a ^< lift.{v} b := by + conv_lhs => simp only [powerlt, lift_iSup, bddAbove_of_small] + apply le_antisymm + · refine ciSup_le' fun c => ?_ + rw [lift_power] + exact le_powerlt _ (lift_lt.2 c.2) + · simp_rw [powerlt_le, lt_lift_iff] + rintro _ ⟨c, hc, rfl⟩ + haveI := Small.trans_univLE.{u, max u v} (Iio b) + refine le_ciSup_of_le bddAbove_of_small ⟨c, hc⟩ ?_ + simp + /-- The cardinality of a set is an upper-bound for the amount of elements before the set's mex (minimum excluded value) -/ theorem _root_.WellFounded.cardinalMk_subtype_lt_min_compl_le {r : α → α → Prop} diff --git a/Mathlib/SetTheory/Cardinal/Cofinality.lean b/Mathlib/SetTheory/Cardinal/Cofinality.lean index e9453815eeeea3..64c181d223831e 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality.lean @@ -502,6 +502,34 @@ theorem _root_.Cardinal.iSup_lt_of_lt_cof_ord {f : α → Cardinal.{u}} {a : Car rw [← ord_lt_ord, iSup_ord] apply Ordinal.iSup_lt_of_lt_cof <;> simpa +theorem bddAbove_Iio_of_lt_cof {o : Ordinal.{u}} {s : Set (Iio o)} + (hs : #s < Cardinal.lift.{u + 1} o.cof) : BddAbove s := by + refine ⟨⟨sSup ((↑) '' s), ?_⟩, ?_⟩ + · apply sSup_lt_of_lt_cof + · rwa [mk_image_eq Subtype.val_injective, ← lift_cof] + · grind + · simp only [mem_upperBounds, ← Subtype.coe_le_coe] + intro x hx + apply le_csSup bddAbove_of_small + grind + +theorem bddAbove_toType_of_lt_cof {o : Ordinal.{u}} {s : Set o.ToType} (hs : #s < o.cof) : + BddAbove s := by + rw [← ToType.mk.bddAbove_preimage] + apply bddAbove_Iio_of_lt_cof + rwa [← Cardinal.lift_id'.{u, u + 1} #_, ← EquivLike.coe_coe, mk_preimage_equiv_lift, + Cardinal.lift_lt] + +theorem bddAbove_range_Iio_of_lt_cof {o : Ordinal.{u}} {ι : Type v} {f : ι → Iio o} + (hι : Cardinal.lift.{u} #ι < Cardinal.lift.{v} o.cof) : BddAbove (Set.range f) := + bddAbove_Iio_of_lt_cof (by + grw [← Cardinal.lift_lt.{_, v}, mk_range_le_lift] + simpa using Cardinal.lift_lt.{_, u + 1}.2 hι) + +theorem bddAbove_range_toType_of_lt_cof {o : Ordinal.{u}} {ι : Type v} {f : ι → o.ToType} + (hι : Cardinal.lift.{u} #ι < Cardinal.lift.{v} o.cof) : BddAbove (Set.range f) := + bddAbove_toType_of_lt_cof (by grw [← Cardinal.lift_lt.{_, v}, mk_range_le_lift]; exact hι) + set_option linter.deprecated false in /-- The set in the `lsub` characterization of `cof` is nonempty. -/ @[deprecated "to build an increasing function with limit o, use the fundamental sequence API." diff --git a/Mathlib/SetTheory/Cardinal/DeltaSystem.lean b/Mathlib/SetTheory/Cardinal/DeltaSystem.lean index d60aa0bb977d8a..540fa7466ed21f 100644 --- a/Mathlib/SetTheory/Cardinal/DeltaSystem.lean +++ b/Mathlib/SetTheory/Cardinal/DeltaSystem.lean @@ -5,7 +5,10 @@ Authors: Dexin Zhang -/ module -public import Mathlib.SetTheory.Cardinal.Pigeonhole +public import Mathlib.SetTheory.Cardinal.Regular + +import Mathlib.Order.Club +import Mathlib.Order.CompleteLatticeIntervals /-! # Δ-systems @@ -27,13 +30,14 @@ contain an uncountable Δ-system. ## TODO -* Prove that `Δ(θ, κ)` is equivalent to `∀ c < θ, c ^< κ < θ` for any regular cardinal `θ` and - infinite cardinal `κ < θ`. (See .) +* Prove that `Δ(θ, κ)` is equivalent to `∀ c < θ, c ^< κ < θ` for any regular `θ` and infinite + `κ < θ`. (See .) * Prove that `Δ(θ, κ)` does not hold for singluar `θ`. ## References * [Kenneth Kunen, *Set Theory: An Introduction to Independence Proofs.*][kunen1980set] +* [Kenneth Kunen, *Set Theory.*][kunen2011set] -/ @[expose] public section @@ -48,10 +52,15 @@ def DeltaSystemProperty (θ κ : Cardinal.{u}) := ∀ ι α (f : ι → Set α), #ι = θ → (∀ i, #(f i) < κ) → ∃ (s : Set ι) (t : Set α), #s = θ ∧ s.Pairwise (f · ∩ f · = t) -variable {θ κ : Cardinal.{u}} +variable {θ κ μ : Cardinal.{u}} open Order Ordinal Set +@[gcongr] +theorem DeltaSystemProperty.mono (h : κ ≤ μ) (hμ : DeltaSystemProperty θ μ) : + DeltaSystemProperty θ κ := + fun ι α f hι hf => hμ ι α f hι fun i => (hf i).trans_le h + /-- An alternative formalization of Δ-system property, with weaker assumption and stronger conclusion. -/ theorem DeltaSystemProperty.exists_pairwise_eq (h : DeltaSystemProperty θ κ) (hκ : 0 < κ) @@ -68,224 +77,128 @@ theorem DeltaSystemProperty.exists_pairwise_eq (h : DeltaSystemProperty θ κ) ( namespace IsRegular -variable (h : κ < θ) (hκ : ℵ₀ ≤ κ) (hθ : θ.IsRegular) (hθ' : ∀ c < θ, c ^< κ < θ) - -include h hκ hθ hθ' in -private lemma delta_system_property_aux {ι : Type u} {ρ : Ordinal.{u}} {f : ι → Set θ.ord.ToType} - (hι : θ ≤ #ι) (hf : ∀ i, #(f i) < κ) (hρ : ρ < κ.ord) (hρ' : ∀ i, typeLT (f i) = ρ) : - ∃ (s : Set ι) (t : Set θ.ord.ToType), θ ≤ #s ∧ s.Pairwise (f · ∩ f · = t) := by - classical - rcases (zero_le ρ).eq_or_lt with rfl | hρ'' - · simp only [type_eq_zero_iff_isEmpty, isEmpty_coe_sort] at hρ' - exact ⟨Set.univ, ∅, by simpa, by simp [hρ', Set.Pairwise]⟩ - simp_rw [← type_toType ρ, type_eq] at hρ' - have g₁ : ∀ i, ρ.ToType ≃o f i := fun i => OrderIso.ofRelIsoLT (Classical.choice (hρ' i)).symm - haveI : Nonempty θ.ord.ToType := by simpa using ((zero_le κ).trans_lt h).ne' - letI := WellFoundedLT.toOrderBot (α := θ.ord.ToType) - letI := WellFoundedLT.conditionallyCompleteLinearOrderBot θ.ord.ToType - by_cases hξ₀ : ∀ ξ : ρ.ToType, Bounded (· < ·) {(g₁ i ξ).1 | i} - · simp only [Bounded, mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff] at hξ₀ - choose b hb using hξ₀ - have : BddAbove (range b) := by - rw [bddAbove_def] - refine ⟨Ordinal.ToType.mk ⟨⨆ x, (b x).toOrd.1, ?_⟩, ?_⟩ - · rw [mem_Iio] - apply iSup_lt_ord_of_isRegular hθ - · simpa [← lt_ord] using hρ.trans (ord_lt_ord.2 h) - · exact fun i => (b i).toOrd.2 - · simp only [mem_range, forall_exists_index, forall_apply_eq_imp_iff, - ← ToType.mk.symm_apply_le, ← Subtype.coe_le_coe] - exact le_ciSup (Ordinal.bddAbove_of_small _) - let b₀ := iSup b - have : ∀ i, Subtype.val '' range (g₁ i) ⊆ Iio b₀ := by - intro i x hx - simp only [mem_image, mem_range, ↓existsAndEq, true_and] at hx - rcases hx with ⟨x, rfl⟩ - exact (hb _ _).trans_le <| le_ciSup this x - simp_rw [← OrderIso.coe_toEquiv, Equiv.range_eq_univ, image_univ, Subtype.range_val] at this - have : #(range f) < θ := by - apply (mk_range_le_powerlt κ (Iio b₀) this hf).trans_lt - rw [mul_eq_max_of_aleph0_le_left hκ] - · simp only [sup_lt_iff, h, true_and] - apply hθ' - simp only [sup_lt_iff, hκ.trans_lt h, and_true] - exact mk_Iio_ord_toType _ - · simpa [powerlt_eq_zero_iff] using (aleph0_pos.trans_le hκ).ne' - rcases infinite_pigeonhole_card_range f θ hι hθ.aleph0_le (by rwa [hθ.cof_eq]) with ⟨t, ht⟩ - refine ⟨_, t, ht, ?_⟩ - grind [Set.Pairwise] - haveI : Nonempty ρ.ToType := by simpa using hρ''.ne' - letI := Classical.inhabited_of_nonempty (α := ρ.ToType) inferInstance - letI := WellFoundedLT.toOrderBot (α := ρ.ToType) - letI := WellFoundedLT.conditionallyCompleteLinearOrderBot ρ.ToType - let ξ₀ : ρ.ToType := sInf {ξ : ρ.ToType | Unbounded (· < ·) {(g₁ i ξ).1 | (i : ι)}} - replace hξ₀ : Unbounded (· < ·) {(g₁ i ξ₀).1 | i} := by - simp_rw [not_forall, not_bounded_iff] at hξ₀ - apply csInf_mem (s := {ξ | Unbounded (· < ·) {(g₁ i ξ).1 | i}}) - simpa [nonempty_def] - have hξ₀' : ∀ ξ < ξ₀, Bounded (· < ·) {(g₁ i ξ).1 | (i : ι)} := by - intro ξ hξ - apply notMem_of_lt_csInf' at hξ - simpa using hξ - choose! α hα using hξ₀' - simp only [mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff] at hα - let α₀ := ⨆ ξ : Iio ξ₀, α ξ - haveI : NoMaxOrder (θ.ord.ToType) := noMaxOrder hθ.aleph0_le - have hα₀ : ∀ i, ∀ ξ < ξ₀, g₁ i ξ < α₀ := by - intro i ξ hξ - rw [← succ_le_iff] - refine le_ciSup_of_le ?_ ⟨ξ, hξ⟩ ?_ - · refine ⟨Ordinal.ToType.mk ⟨⨆ ξ : Iio ξ₀, α ξ, ?_⟩, ?_⟩ - · rw [mem_Iio] - apply iSup_lt_ord_of_isRegular hθ - · apply (mk_set_le _).trans_lt - apply h.trans' - simpa [← lt_ord] - · exact fun i => (α i).toOrd.2 - · simp only [mem_upperBounds, mem_range, Subtype.exists, mem_Iio, exists_prop, - ← ToType.mk.symm_apply_le, ← Subtype.coe_le_coe, forall_exists_index, and_imp, - forall_apply_eq_imp_iff₂] - intro ξ hξ - exact le_ciSup (Ordinal.bddAbove_range _) (⟨ξ, hξ⟩ : Iio ξ₀) - · rw [succ_le_iff] - exact hα ξ hξ i - haveI : Nonempty ι := by simpa [← mk_ne_zero_iff] using hθ.pos.trans_le hι |>.ne' - let g₂ : θ.ord.ToType → ι := WellFoundedLT.fix fun x ih => - Classical.epsilon fun i => α₀ < g₁ i ξ₀ ∧ ∀ y hy ξ, (g₁ (ih y hy) ξ).1 < g₁ i ξ₀ - have hg₂ : ∀ μ, α₀ < g₁ (g₂ μ) ξ₀ ∧ ∀ ν < μ, ∀ ξ, (g₁ (g₂ ν) ξ).1 < g₁ (g₂ μ) ξ₀ := by - intro μ - suffices ∃ i, α₀ < g₁ i ξ₀ ∧ ∀ ν < μ, ∀ ξ, (g₁ (g₂ ν) ξ).1 < g₁ i ξ₀ by - apply Classical.epsilon_spec at this - unfold g₂ - rwa [WellFoundedLT.fix_eq] - let o : Ordinal := succ (max α₀ (⨆ ν : Iio μ, ⨆ ξ, g₁ (g₂ ν) ξ)) - have ho : o < θ.ord := by - apply (Cardinal.isSuccLimit_ord hθ.aleph0_le).succ_lt - refine max_lt α₀.toOrd.2 ?_ - apply iSup_lt_ord_of_isRegular hθ - · apply mk_Iio_ord_toType - · intro - apply iSup_lt_ord_of_isRegular hθ - · apply h.trans' - simpa [← lt_ord] - · exact fun _ => (Ordinal.ToType.toOrd _).2 - rcases hξ₀ (Ordinal.ToType.mk ⟨o, ho⟩) with ⟨_, ⟨i, rfl⟩, hi⟩ - simp only [not_lt, ← ToType.mk.le_symm_apply, ← Subtype.coe_le_coe, succ_le_iff, sup_lt_iff, - Subtype.coe_lt_coe, OrderIso.lt_iff_lt, o] at hi - rcases hi with ⟨hi₁, hi₂⟩ - refine ⟨i, hi₁, fun ν hν ξ => ?_⟩ - rw [← ToType.mk.symm.lt_iff_lt] - apply hi₂.trans_le' - exact le_ciSup_of_le (Ordinal.bddAbove_range _) ⟨ν, hν⟩ <| - le_ciSup_of_le (Ordinal.bddAbove_range _) ξ le_rfl - have hg₂' : Function.Injective g₂ := by - intro x y h - by_contra! h' - rcases lt_or_gt_of_ne h' with h' | h' - · have := (hg₂ _).2 _ h' ξ₀ - rw [h] at this - simp at this - · have := (hg₂ _).2 _ h' ξ₀ - rw [h] at this - simp at this - have hg₂'' : ∀ x y, x ≠ y → f (g₂ x) ∩ f (g₂ y) ⊆ Iio α₀ := by - intro x y h - wlog h' : x < y generalizing x y - · rw [inter_comm] - exact this _ _ h.symm (lt_of_le_of_ne (le_of_not_gt h') h.symm) - intro z - simp only [mem_inter_iff, mem_Iio, and_imp] - intro hzx hzy - by_contra hz - let ξx := (g₁ (g₂ x)).symm ⟨z, hzx⟩ - let ξy := (g₁ (g₂ y)).symm ⟨z, hzy⟩ - have hξy : ξ₀ ≤ ξy := by - by_contra! - apply hα₀ (g₂ y) at this - simp only [OrderIso.apply_symm_apply, ξy] at this - contradiction - simp only [(g₁ (g₂ y)).le_symm_apply, ← Subtype.coe_le_coe, ξy] at hξy - apply ((hg₂ _).2 _ h' ξx).trans_le at hξy - simp [ξx] at hξy - let g₃ : θ.ord.ToType → Set θ.ord.ToType := fun x => f (g₂ x) ∩ Set.Iio α₀ - have hg₃ : ∀ x, g₃ x ⊆ Set.Iio α₀ := by simp [g₃] - have hg₃' : #(Set.range g₃) < θ := by - refine (mk_range_le_powerlt κ (Iio α₀) hg₃ ?_).trans_lt ?_ - · intro i - refine (mk_le_mk_of_subset ?_).trans_lt (hf (g₂ i)) - grind - · rw [mul_eq_max_of_aleph0_le_left hκ] - · apply max_lt h - apply hθ' - apply max_lt - · exact mk_Iio_ord_toType _ - · exact hκ.trans_lt h - · simp [powerlt_eq_zero_iff, (aleph0_pos.trans_le hκ).ne'] - rcases infinite_pigeonhole_card_range g₃ θ (by rw [mk_ord_toType]) hθ.aleph0_le - (by rwa [hθ.cof_eq]) with ⟨r, hr⟩ - refine ⟨g₂ '' (g₃ ⁻¹' {r}), r, ?_, ?_⟩ - · rwa [mk_image_eq hg₂'] - · apply Pairwise.image - intro x hx y hy hxy - simp only [mem_preimage, mem_singleton_iff, g₃] at hx hy - simpa [← inter_inter_distrib_right, inter_self, inter_eq_left.2 (hg₂'' x y hxy)] - using congr_arg₂ (· ∩ ·) hx hy +private lemma deltaSystemProperty_aux (hκμ : κ ≤ μ) (hμθ : μ < θ) (hκ : ℵ₀ ≤ κ) (hμ : μ.IsRegular) + (hθ : θ.IsRegular) (hθ' : ∀ c < θ, c ^< κ < θ) {f : Iio θ.ord → Set (Iio θ.ord)} + (hf : ∀ i, #(f i) < Cardinal.lift.{u + 1} κ) : + ∃ (s : Set (Iio θ.ord)) (t : Set (Iio θ.ord)), + #s = Cardinal.lift.{u + 1} θ ∧ s.Pairwise (f · ∩ f · = t) := by + haveI : Nonempty (Iio θ.ord) := ⟨0, by simp [hθ.pos]⟩ + haveI : NoMaxOrder (Iio θ.ord) := noMaxOrder_Iio_ord hθ.aleph0_le + haveI : Fact (¬ IsMin θ.ord) := ⟨by simp [← pos_iff_ne_zero, hθ.pos]⟩ + have : ℵ₀ < Order.cof (Iio θ.ord) := by + simpa [← lift_ord, ← lift_cof, hθ.cof_ord] using hμ.aleph0_le.trans_lt hμθ + have : typeLT (Iio θ.ord) ≤ (Order.cof (Iio θ.ord)).ord := by + simp [← lift_ord, ← lift_cof, hθ.cof_ord] + rcases exists_isStationary_preimage_singleton (f := fun i => sSup (Set.Iio i ∩ f i)) + (by assumption) (by assumption) (hθ.isStationary_setOf_cof_eq hμ hμθ) + (by + intro ⟨i, hi⟩ + simp only [mem_setOf_eq, gt_iff_lt] at hi ⊢ + rw [← Subtype.coe_lt_coe, Iio.coe_sSup (bddAbove_Iio.mono inter_subset_left)] + apply Ordinal.sSup_lt_of_lt_cof + · grw [mk_image_eq Subtype.val_injective, mk_le_mk_of_subset inter_subset_right] + apply (hf i).trans_le + simpa [← lift_cof, hi] + · simp +contextual [← Subtype.coe_lt_coe]) with ⟨ξ, hξ⟩ + have : ∃ ν : Iio θ.ord, ξ < ν := by + rcases (isSuccLimit_ord hθ.aleph0_le).lt_iff_exists_lt.1 ξ.2 with ⟨ν, hν, hν'⟩ + exact ⟨⟨ν, hν⟩, hν'⟩ + rcases this with ⟨ν, hν⟩ + rcases exists_isStationary_preimage_singleton_of_cardinalMk_range_lt_cof + (f := fun i => f i ∩ Iio ν) (by assumption) + (hξ.inter_isClub (by assumption) + (isClub_almost_fixed_points (f := sSup ∘ f) (by assumption) (by assumption))) + (by + grw [mk_range_le_powerlt (Cardinal.lift.{u + 1} κ) (Iio ν)] + · rw [mk_Iio_Iio_ord_eq, ← lift_aleph0.{u + 1, u}] + simp only [← lift_max, ← lift_powerlt, ← lift_mul, Ordinal.cof_Iio, ← lift_cof, lift_lt] + rw [hθ.cof_ord, mul_eq_max_of_aleph0_le_left hκ] + · refine max_lt (hκμ.trans_lt hμθ) (hθ' _ (max_lt ?_ (hμ.aleph0_le.trans_lt hμθ))) + rw [← lt_ord] + exact ν.2 + · simpa [powerlt_eq_zero_iff] using pos_iff_ne_zero.1 (aleph0_pos.trans_le hκ) + · grind + · exact fun i => (mk_le_mk_of_subset inter_subset_left).trans_lt (hf _)) with ⟨w, hw⟩ + refine ⟨_, w, hθ.card_eq_of_isStationary hw, ?_⟩ + intro i hi j hj hij + wlog hij' : i < j generalizing i j + · rw [inter_comm] + exact this hj hi hij.symm (lt_of_le_of_ne (le_of_not_gt hij') hij.symm) + simp only [mem_setOf_eq, coe_setOf, Function.comp_apply, mem_image, mem_preimage, + mem_singleton_iff, Subtype.exists, mem_inter_iff, exists_and_left, exists_prop, + exists_eq_right_right] at hi hj + rcases hi with ⟨hi₁, ⟨-, hi₃⟩, hi₄⟩ + rcases hj with ⟨hj₁, ⟨hj₂, hj₃⟩, hj₄⟩ + nth_rw 1 [← inter_self w, ← hi₁, ← hj₁, ← inter_inter_distrib_right, + inter_eq_self_of_subset_left (t := Iio ν)] + intro x hx + simp only [mem_inter_iff, mem_Iio] at hx ⊢ + apply hν.trans_le' + rw [← hj₂] + apply le_csSup (bddAbove_Iio.mono inter_subset_left) + simp only [mem_inter_iff, mem_Iio, hx.2, and_true] + apply (hj₄ _ hij').trans_le' + refine le_csSup (bddAbove_Iio_of_lt_cof ?_) hx.1 + grw [hf] + simpa [hθ.cof_ord] using hκμ.trans_lt hμθ -include h hκ hθ hθ' in /-- **Δ-system lemma**: `Δ(θ, κ)` holds for any regular cardinal `θ` and infinite cardinal `κ < θ` such that `∀ c < θ, c ^< κ < θ`. -/ -theorem delta_system_property_of_powerlt_lt : DeltaSystemProperty θ κ := by +theorem deltaSystemProperty_of_powerlt_lt (h : κ < θ) (hκ : ℵ₀ ≤ κ) (hθ : θ.IsRegular) + (hθ' : ∀ c < θ, c ^< κ < θ) : DeltaSystemProperty θ κ := by intro ι α f hι hf - haveI : Nonempty ι := by - simpa [mk_ne_zero_iff] using (aleph0_pos.trans_le hκ |>.trans h |>.trans_le hι.ge).ne' + have : ∃ μ ≥ κ, μ < θ ∧ μ.IsRegular := by + rcases lt_or_eq_of_le (cof_ord_le κ) with hκ' | hκ' + · refine ⟨Order.succ κ, Order.le_succ _, ?_, isRegular_succ hκ⟩ + apply (hθ' _ h).trans_le' + rw [Order.succ_le_iff] + apply (lt_power_cof_ord hκ).trans_le + exact le_powerlt _ hκ' + · exact ⟨κ, le_rfl, h, hκ, hκ'.ge⟩ + rcases this with ⟨μ, hμ, hμ', hμ''⟩ + haveI : Nonempty ι := by simp [← mk_ne_zero_iff, hι, ← pos_iff_ne_zero, hθ.pos] have : #(⋃ i, f i) ≤ θ := by refine mk_iUnion_le_sum_mk.trans <| (sum_le_mk_mul_iSup _).trans <| - (mul_le_mul_right (ciSup_mono (bddAbove_of_small _) fun i => (hf i).le) _).trans ?_ + (mul_le_mul_right (ciSup_mono bddAbove_of_small fun i => (hf i).le) _).trans ?_ rw [ciSup_const, mul_eq_left (hκ.trans h.le |>.trans hι.ge) (h.le.trans hι.ge) (aleph0_pos.trans_le hκ).ne', hι] - rw [← card_ord θ, ← mk_toType, le_def] at this + rw [← card_ord θ, ← Cardinal.lift_le, ← mk_Iio_ordinal, ← Cardinal.lift_id #(Iio θ.ord), + Cardinal.lift_mk_le.{u + 1}] at this rcases this with ⟨g⟩ - let g' : ι → Set θ.ord.ToType := fun i => - Set.range ((Set.embeddingOfSubset _ _ (Set.subset_iUnion f i)).trans g) - have hg : ∀ i, #(g' i) < κ := fun i => mk_range_le.trans_lt (hf i) - have hg' : ∀ i, typeLT (g' i) < κ.ord := by simpa [lt_ord, card_type] - rcases infinite_pigeonhole_card (fun i => Ordinal.ToType.mk ⟨typeLT (g' i), hg' i⟩) _ hι.ge - (hκ.trans h.le) (by rwa [mk_ord_toType, hθ.cof_eq]) with ⟨ρ, hs⟩ - generalize hρ : (_ ⁻¹' {ρ}) = s at hs - have : ∃ ρ', ρ = Ordinal.ToType.mk ρ' := ⟨ρ.toOrd, by simp⟩ - rcases this with ⟨⟨ρ, hρ'⟩, rfl⟩ - simp only [mem_Iio] at hρ' - apply (subset_of_eq ∘ Eq.symm) at hρ - simp_rw [subset_def, mem_preimage, mem_singleton_iff, ToType.mk.eq_iff_eq, Subtype.mk_eq_mk] - at hρ - rcases delta_system_property_aux (ι := s) (f := g' ∘ Subtype.val) h hκ hθ hθ' hs (by grind) hρ' - (by grind) with ⟨s', t, hs', ht⟩ - refine ⟨Subtype.val '' s', Subtype.val '' (g ⁻¹' t), ?_, ?_⟩ - · rw [mk_image_eq Subtype.val_injective] - refine hs'.antisymm' <| (mk_set_le _).trans <| (mk_set_le _).trans ?_ - rw [hι] - · refine .image (ht.imp fun x y h => ?_) - simp only [Function.comp_apply] at h - rw [Function.onFun_apply, ← h, preimage_inter, image_inter Subtype.val_injective] + rw [← Cardinal.lift_inj.{u, u + 1}, ← card_ord θ, ← mk_Iio_ordinal, + ← Cardinal.lift_id #(Iio θ.ord), Cardinal.lift_mk_eq.{u, u + 1, u + 1}] at hι + rcases hι with ⟨e⟩ + rcases deltaSystemProperty_aux + (f := fun i => Set.range ((Set.embeddingOfSubset _ _ (Set.subset_iUnion f (e.symm i))).trans g)) + hμ hμ' hκ hμ'' hθ hθ' (fun _ => by + rw [← Cardinal.lift_id'.{u, u + 1} #_, + mk_range_eq_of_injective (Function.Embedding.injective _), Cardinal.lift_lt] + apply hf) with ⟨s, t, hs, ht⟩ + refine ⟨e.symm '' s, Subtype.val '' (g ⁻¹' t), ?_, ?_⟩ + · rw [← Cardinal.lift_inj, mk_image_eq_of_injOn_lift _ _ e.symm.injective.injOn] + simp [hs] + · refine .image (ht.imp fun i j h => ?_) + simp only [← h, preimage_inter, image_inter Subtype.val_injective, Function.onFun_apply] congr <;> ext i <;> simp only [embeddingOfSubset, mem_image, mem_preimage, mem_range, - Function.Embedding.trans_apply, Function.Embedding.coeFn_mk, Subtype.exists, g'] <;> grind + Function.Embedding.trans_apply, Function.Embedding.coeFn_mk, EmbeddingLike.apply_eq_iff_eq, + Subtype.exists] <;> grind -include hθ in /-- `Δ(θ, ℵ₀)` holds for any uncountable regular cardinal `θ`. -/ -theorem delta_system_property_aleph0 (hθ' : ℵ₀ < θ) : DeltaSystemProperty θ ℵ₀ := by - apply delta_system_property_of_powerlt_lt hθ' le_rfl hθ +theorem deltaSystemProperty_aleph0 (hθ : θ.IsRegular) (hθ' : θ ≠ ℵ₀) : + DeltaSystemProperty θ ℵ₀ := by + replace hθ' := hθ.aleph0_le.lt_of_ne' hθ' + apply deltaSystemProperty_of_powerlt_lt hθ' le_rfl hθ intro c hc apply (powerlt_aleph0_le _).trans_lt simp [hc, hθ'] -include hθ in /-- **Δ-system lemma** for `Δ(θ, ℵ₀)`: for any uncountable regular cardinal `θ`, any `θ`-sized family of finite sets must contain a `θ`-sized Δ-system. -/ -theorem exists_pairwise_inter_eq_finset (hθ' : ℵ₀ < θ) {ι : Type u} {α : Type v} [DecidableEq α] - (f : ι → Finset α) (hι : θ ≤ #ι) : +theorem exists_pairwise_inter_eq_finset (hθ : θ.IsRegular) (hθ' : θ ≠ ℵ₀) {ι : Type u} {α : Type v} + [DecidableEq α] (f : ι → Finset α) (hι : θ ≤ #ι) : ∃ (s : Set ι) (t : Finset α), #s = θ ∧ s.Pairwise (f · ∩ f · = t) := by - rcases (delta_system_property_aleph0 hθ.lift (aleph0_lt_lift.{u, v}.2 hθ')).exists_pairwise_eq + rcases (deltaSystemProperty_aleph0 hθ.lift (by simpa)).exists_pairwise_eq aleph0_pos (f := fun i : ULift.{v} ι => Equiv.ulift.symm '' (f i.down : Set α)) (by simpa) (by simp) with ⟨s, t, hs, ht, ht'⟩ rw [lt_aleph0_iff_subtype_finite, setOf_mem_eq] at ht @@ -307,7 +220,7 @@ uncountable Δ-system. -/ theorem Uncountable.exists_pairwise_inter_eq_finset {ι : Type u} {α : Type v} [Uncountable ι] [DecidableEq α] (f : ι → Finset α) : ∃ (s : Set ι) (t : Finset α), Uncountable s ∧ s.Pairwise (f · ∩ f · = t) := by - rcases isRegular_aleph_one.exists_pairwise_inter_eq_finset aleph0_lt_aleph_one f - (by simp [← succ_aleph0]) with ⟨s, t, hs, ht⟩ + rcases isRegular_aleph_one.exists_pairwise_inter_eq_finset aleph0_lt_aleph_one.ne' f (by simp) + with ⟨s, t, hs, ht⟩ refine ⟨s, t, ?_, ht⟩ - simpa [← aleph0_lt_mk_iff, hs] using aleph0_lt_aleph_one + simp [← aleph0_lt_mk_iff, hs] diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean index 8c797650a645c1..9872ab9d23f347 100644 --- a/Mathlib/SetTheory/Ordinal/Arithmetic.lean +++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean @@ -1189,6 +1189,9 @@ theorem noMaxOrder {c} (h : ℵ₀ ≤ c) : NoMaxOrder c.ord.ToType := by rw [← isSuccPrelimit_type_lt_iff, type_toType] exact (isSuccLimit_ord h).isSuccPrelimit +theorem noMaxOrder_Iio_ord {c} (h : ℵ₀ ≤ c) : NoMaxOrder (Iio c.ord) := + (isSuccLimit_ord h).isSuccPrelimit.noMaxOrder_Iio + instance : Nonempty (ℵ₀ : Cardinal.{u}).ord.ToType := by simp /-- This can be made a local instance in order to get `⊥` diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index 327d83ba1c07d4..e10213f6a91660 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -533,6 +533,8 @@ def ToType.mk {o : Ordinal} : Set.Iio o ≃o o.ToType where /-- Convert an element of `α.toType` to the corresponding `Ordinal` -/ abbrev ToType.toOrd {o : Ordinal} (α : o.ToType) : Set.Iio o := ToType.mk.symm α +instance {o : Ordinal} : WellFoundedLT (Set.Iio o) := ToType.mk.toOrderEmbedding.wellFoundedLT + instance (o : Ordinal) : Coe o.ToType (Set.Iio o) where coe := ToType.toOrd instance (o : Ordinal) : CoeOut o.ToType Ordinal where @@ -1188,6 +1190,10 @@ theorem mk_Iio_lt [LinearOrder α] [WellFoundedLT α] (i : α) (h : ord #α = ty theorem mk_Iio_toType_ord_lt {c : Cardinal} (i : c.ord.ToType) : #(Iio i) < c := by simpa using mk_Iio_lt i +theorem mk_Iio_Iio_ord_lt {c : Cardinal.{u}} (i : Iio c.ord) : + #(Iio i) < Cardinal.lift.{u + 1} c := by + simpa using mk_Iio_lt i + @[deprecated (since := "2026-03-20")] alias mk_Iio_ord_toType := mk_Iio_toType_ord_lt set_option linter.deprecated false in @@ -1196,6 +1202,10 @@ theorem card_typein_toType_lt (c : Cardinal) (x : c.ord.ToType) : card (typein (α := c.ord.ToType) (· < ·) x) < c := mk_Iio_toType_ord_lt x +theorem mk_Iio_Iio_ord_eq {c : Cardinal.{u}} (i : Iio c.ord) : + #(Iio i) = Cardinal.lift.{u + 1} i.1.card := by + rw [← mk_Iio_ordinal, ← Set.image_subtype_val_Iio_Iio, mk_image_eq Subtype.val_injective] + theorem ord_injective : Injective ord := by intro c c' h rw [← card_ord c, ← card_ord c', h] diff --git a/docs/references.bib b/docs/references.bib index f4ee20d760a0b9..0195f945f4c748 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -3555,6 +3555,13 @@ @Book{ kunen1980set publisher = {North Holland, Amsterdam} } +@Book{ kunen2011set, + title = {Set theory}, + author = {Kunen, Kenneth}, + year = {2011}, + publisher = {College Publications, London} +} + @Book{ kung_rota_yan2009, author = {Kung, Joseph P. S. and Rota, Gian-Carlo and Yan, Catherine H.},