diff --git a/Mathlib.lean b/Mathlib.lean index 4126812cdba773..8318a10440b849 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 @@ -6887,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/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/Club.lean b/Mathlib/Order/Club.lean new file mode 100644 index 00000000000000..678ccffba70f92 --- /dev/null +++ b/Mathlib/Order/Club.lean @@ -0,0 +1,330 @@ +/- +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.Regular +public import Mathlib.Order.DirSupClosed + +import Mathlib.Data.Set.Monotone +import Mathlib.Order.CompleteLatticeIntervals + +/-! +# 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 set is called **stationary** when it intersects all club sets. + +## 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 Ordinal + +/-! ### Club sets -/ + +/-- A club set is closed under suprema and cofinal. -/ +structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where + /-- Club sets are closed under suprema. If `α` is a well-order with the order topology, this + condition is equivalent to `IsClosed s`. -/ + dirSupClosed : DirSupClosed s + /-- Club sets are cofinal. If `α` has no maximum, this condition is equivalent to `¬ BddAbove s`. + See `not_bddAbove_iff_isCofinal`. -/ + isCofinal : IsCofinal s + +variable {α : Type v} {s t : Set α} {x : α} [LinearOrder α] + +@[simp] +theorem IsClub.of_isEmpty [IsEmpty α] (s : Set α) : IsClub s := + ⟨.of_isEmpty s, .of_isEmpty s⟩ + +@[simp] +theorem IsClub.univ : IsClub (.univ (α := α)) := + ⟨.univ, .univ⟩ + +theorem isClub_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) + +theorem IsClub.isLUB_mem (hs : IsClub s) (ht : t ⊆ s) (ht₀ : t.Nonempty) (hx : IsLUB t x) : x ∈ s := + hs.dirSupClosed ht ht₀ (Std.Total.directedOn _) hx + +theorem IsClub.csSup_mem {α} [ConditionallyCompleteLinearOrder α] {s t : Set α} + (hs : IsClub s) (ht : t ⊆ s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) : sSup t ∈ s := + hs.isLUB_mem ht ht₀ (isLUB_csSup ht₀ ht₁) + +theorem IsClub.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' + +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 α] + +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.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] + 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⟩ + rw [Set.mem_Ici, hgm.le_iff_le, Nat.add_one_le_iff] at hm + cases m with + | zero => contradiction + | succ m => + dsimp + rw [g.iterate_succ_apply'] + 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α : ℵ₀ < 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'] + · 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) + +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 -/ + +/-- 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.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 + 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ᶜ) + +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`. -/ +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⟩)⟩ + +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/CompleteLatticeIntervals.lean b/Mathlib/Order/CompleteLatticeIntervals.lean index d55d8efcda1b5b..fd9e8c601bbef1 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 linear order 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/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean index 803eeec2c4672a..74c6d1736e83f4 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 @@ -62,6 +63,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) @@ -157,24 +174,90 @@ 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 a) + rw [← isLUB_congr_of_antisymmRel h] + exact isLUB_singleton -lemma IsLowerSet.dirSupInacc (hs : IsLowerSet s) : DirSupInacc s := hs.compl.dirSupClosed.of_compl +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⟩ -lemma dirSupClosed_Iic (a : α) : DirSupClosed (Iic a) := fun _d h _ _ _a ha ↦ (isLUB_le_iff ha).2 h +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 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 + +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 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/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 diff --git a/Mathlib/SetTheory/Cardinal/Arithmetic.lean b/Mathlib/SetTheory/Cardinal/Arithmetic.lean index 9a2488ce06242c..e5d7cacc7dc335 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..f939509dbdce4f 100644 --- a/Mathlib/SetTheory/Cardinal/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Basic.lean @@ -1037,6 +1037,15 @@ 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 + +@[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) @@ -1057,6 +1066,32 @@ 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 [← Cardinal.one_le_iff_pos] at hb ⊢ + 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 d071036b42ae89..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." @@ -741,6 +769,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 diff --git a/Mathlib/SetTheory/Cardinal/DeltaSystem.lean b/Mathlib/SetTheory/Cardinal/DeltaSystem.lean new file mode 100644 index 00000000000000..540fa7466ed21f --- /dev/null +++ b/Mathlib/SetTheory/Cardinal/DeltaSystem.lean @@ -0,0 +1,226 @@ +/- +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.Regular + +import Mathlib.Order.Club +import Mathlib.Order.CompleteLatticeIntervals + +/-! +# Δ-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 `θ` 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 + +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 + +@[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 < κ) + {ι α : 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 + +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μθ + +/-- **Δ-system lemma**: `Δ(θ, κ)` holds for any regular cardinal `θ` and infinite cardinal `κ < θ` +such that `∀ c < θ, c ^< κ < θ`. -/ +theorem deltaSystemProperty_of_powerlt_lt (h : κ < θ) (hκ : ℵ₀ ≤ κ) (hθ : θ.IsRegular) + (hθ' : ∀ c < θ, c ^< κ < θ) : DeltaSystemProperty θ κ := by + intro ι α f hι hf + 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 ?_ + 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 θ, ← Cardinal.lift_le, ← mk_Iio_ordinal, ← Cardinal.lift_id #(Iio θ.ord), + Cardinal.lift_mk_le.{u + 1}] at this + rcases this with ⟨g⟩ + 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, EmbeddingLike.apply_eq_iff_eq, + Subtype.exists] <;> grind + +/-- `Δ(θ, ℵ₀)` holds for any uncountable regular cardinal `θ`. -/ +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θ'] + +/-- **Δ-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θ : θ.IsRegular) (hθ' : θ ≠ ℵ₀) {ι : Type u} {α : Type v} + [DecidableEq α] (f : ι → Finset α) (hι : θ ≤ #ι) : + ∃ (s : Set ι) (t : Finset α), #s = θ ∧ s.Pairwise (f · ∩ f · = t) := by + 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 + 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.ne' f (by simp) + with ⟨s, t, hs, ht⟩ + refine ⟨s, t, ?_, ht⟩ + simp [← aleph0_lt_mk_iff, hs] 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/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 41efdc683252b3..0195f945f4c748 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -3548,6 +3548,20 @@ @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{ 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.},