From 4810229c1795ab26663e1a5c80de53ad562e9640 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 22 May 2026 14:24:22 -0600 Subject: [PATCH 01/24] start --- .../SetTheory/Cardinal/Cofinality/Club.lean | 51 +++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index 58671ac506a2db..8b28e08548d621 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -144,3 +144,54 @@ theorem Order.IsNormal.isClub_fixedPoints {f : α → α} (hα : cof α ≠ ℵ 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. -/ +@[expose] +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 [IsStationary, ← not_imp_not (b := IsClub _), Set.not_nonempty_iff_eq_empty, + isClub_empty_iff] + +@[simp] +theorem IsStationary.univ [Nonempty α] : IsStationary (.univ (α := α)) := + isStationary_univ_iff.2 ‹_› + +@[simp] +theorem not_isStationary_empty : ¬ IsStationary (∅ : Set α) := by + intro h + simpa using h .univ + +theorem IsClub.isStationary [Nonempty α] [WellFoundedLT α] (hα : cof α ≠ ℵ₀) (hs : IsClub s) : + IsStationary s := + fun t ht ↦ (hs.inter hα ht).nonempty + +/-- Non-stationary sets form an ideal. -/ +theorem not_isStationary_union [WellFoundedLT α] (hα : cof α ≠ ℵ₀) + (hs : ¬ IsStationary s) (ht : ¬ IsStationary t) : ¬ IsStationary (s ∪ t) := by + simp_rw [IsStationary, not_forall, Set.not_nonempty_iff_eq_empty] at hs ht ⊢ + obtain ⟨u, hu, hsu⟩ := hs + obtain ⟨v, hv, htv⟩ := ht + refine ⟨_, hu.inter hα hv, ?_⟩ + grind + +theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal (sᶜ)) : IsStationary s := by + intro t ht + obtain ⟨a, ha⟩ := not_isCofinal_iff.1 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α : cof α ≤ ℵ₀) : + IsStationary s ↔ ¬ IsCofinal (sᶜ) From 41a7add19d3b1932309f458e628105609419806c Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 22 May 2026 14:25:14 -0600 Subject: [PATCH 02/24] more --- Mathlib/SetTheory/Cardinal/Cofinality/Club.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index 8b28e08548d621..3382aa467ac76a 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -48,6 +48,12 @@ theorem IsClub.of_isEmpty [IsEmpty α] {s : Set α} : IsClub s := theorem IsClub.univ : IsClub (α := α) .univ := ⟨.univ, .univ⟩ +protected theorem IsClub.nonempty [Nonempty α] (hs : IsClub s) : s.Nonempty := + hs.isCofinal.nonempty + +theorem _root_.isClub_empty_iff : IsClub (α := α) ∅ ↔ IsEmpty α := + ⟨fun h ↦ isCofinal_empty_iff.1 h.isCofinal, fun _ ↦ .of_isEmpty⟩ + theorem IsClub.union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) := ⟨hs.dirSupClosed.union ht.dirSupClosed, hs.isCofinal.mono Set.subset_union_left⟩ From ee445e07229f3f814acbddc7e4638daf32aa6af1 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 22 May 2026 14:26:13 -0600 Subject: [PATCH 03/24] more --- Mathlib/Order/Cofinal.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Mathlib/Order/Cofinal.lean b/Mathlib/Order/Cofinal.lean index 0e8b480d90627f..c3376807934a07 100644 --- a/Mathlib/Order/Cofinal.lean +++ b/Mathlib/Order/Cofinal.lean @@ -53,6 +53,11 @@ theorem IsCofinal.mono {s t : Set α} (h : s ⊆ t) (hs : IsCofinal s) : IsCofin obtain ⟨b, hb, hb'⟩ := hs a exact ⟨b, h hb, hb'⟩ +theorem IsCofinal.nonempty [Nonempty α] {s : Set α} (h : IsCofinal s) : s.Nonempty := by + inhabit α + obtain ⟨x, hx, _⟩ := h default + exact ⟨x, hx⟩ + end LE section Preorder From a8dd5605e1e9890b2f675c54842e9f8c96b05fd8 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 22 May 2026 16:07:01 -0600 Subject: [PATCH 04/24] a lot --- Mathlib/Data/Fintype/Order.lean | 8 ++++++ Mathlib/Order/DirSupClosed.lean | 26 ++++++++++++++++++- .../SetTheory/Cardinal/Cofinality/Basic.lean | 3 +++ .../SetTheory/Cardinal/Cofinality/Club.lean | 25 +++++++++++------- .../Cardinal/Cofinality/Ordinal.lean | 23 ++++++++++++++-- Mathlib/SetTheory/Ordinal/Basic.lean | 4 +++ 6 files changed, 77 insertions(+), 12 deletions(-) diff --git a/Mathlib/Data/Fintype/Order.lean b/Mathlib/Data/Fintype/Order.lean index e4a5f7b738f08f..b02781ca86ac7d 100644 --- a/Mathlib/Data/Fintype/Order.lean +++ b/Mathlib/Data/Fintype/Order.lean @@ -195,6 +195,14 @@ lemma Directed.finite_le {ι κ : Sort*} [Nonempty ι] [Finite κ] {f : ι → simpa using (hf.comp_of_surjective PLift.down_surjective).finite_set_le (Set.finite_range (PLift.up ∘ g)) +theorem DirectedOn.finite_le {s : Set α} (hs₀ : s.Nonempty) (D : DirectedOn r s) + (hs : s.Finite) : ∃ z ∈ s, ∀ i ∈ s, r i z := by + have := hs₀.to_subtype + have := hs.to_subtype + obtain ⟨⟨z, hzs⟩, hz⟩ := D.directed_val.finite_le id + use z, hzs + simpa using hz + variable [Nonempty α] [Preorder α] theorem Finite.exists_le [IsDirectedOrder α] (f : β → α) : ∃ M, ∀ i, f i ≤ M := diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean index ead09bf1ac225a..e6401757f06c46 100644 --- a/Mathlib/Order/DirSupClosed.lean +++ b/Mathlib/Order/DirSupClosed.lean @@ -5,11 +5,12 @@ Authors: Christopher Hoskin, Violeta Hernández Palacios -/ module +public import Mathlib.Data.Fintype.Order public import Mathlib.Order.Antisymmetrization public import Mathlib.Order.CompleteLattice.Defs public import Mathlib.Order.UpperLower.Basic -import Mathlib.Data.Set.Lattice +import Mathlib.Data.Nat.Lattice /-! # Sets closed under directed suprema @@ -300,6 +301,29 @@ theorem dirSupClosed_singleton (a : α) : DirSupClosed {a} := by theorem dirSupClosedOn_singleton (a : α) : DirSupClosedOn D {a} := (dirSupClosed_singleton a).dirSupClosedOn +theorem DirSupClosed.of_finite (hs : s.Finite) : DirSupClosed s := by + intro t ht ht₀ ht₁ a ha + obtain ⟨b, hbt, hb⟩ := ht₁.finite_le ht₀ (hs.subset ht) + exact ht <| ha.unique ⟨hb, fun x hx ↦ hx hbt⟩ ▸ hbt + +theorem dirSupClosed_range_nat {f : ℕ → α} (hf : Monotone f) (hf' : IsCofinal (.range f)) : + DirSupClosed (range f) := by + intro s hs hs₀ hs₁ a ha + obtain ⟨_, ⟨n, rfl⟩, han⟩ := hf' a + obtain rfl | han := han.eq_or_lt + · simp + have hfb : BddAbove (f ⁻¹' s) := by + refine ⟨n, fun m hm ↦ ?_⟩ + by_contra! hnm + exact (ha.1 hm).not_gt (han.trans_le (hf hnm.le)) + refine ⟨sSup (f ⁻¹' s), IsLUB.unique ⟨?_, ?_⟩ ha⟩ <;> intro x hx + · obtain ⟨m, rfl⟩ := hs hx + exact hf (le_csSup hfb hx) + · apply hx (Nat.sSup_mem _ hfb) + obtain ⟨x, hx⟩ := hs₀ + obtain ⟨m, rfl⟩ := hs hx + exact ⟨m, hx⟩ + end PartialOrder section LinearOrder diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean index ff288badfea0f4..54a8ed9659b53f 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean @@ -131,6 +131,9 @@ theorem cof_congr_of_strictMono {f : α → γ} (hf : StrictMono f) (hf' : IsCof cof α = cof γ := by simpa using lift_cof_congr_of_strictMono hf hf' +theorem cof_eq_of_isCofinal {s : Set α} (hs : IsCofinal s) : cof s = cof α := + cof_congr_of_strictMono (Subtype.strictMono_coe _) (by simpa) + @[simp] theorem cof_lt_aleph0_iff : Order.cof α < ℵ₀ ↔ Order.cof α ≤ 1 := by refine ⟨fun h ↦ ?_, (lt_of_le_of_lt · one_lt_aleph0)⟩ diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index 3382aa467ac76a..7749083bbce226 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -5,9 +5,7 @@ Authors: Violeta Hernández Palacios -/ module -public import Mathlib.Order.DirSupClosed -public import Mathlib.Order.IsNormal -public import Mathlib.SetTheory.Cardinal.Cofinality.Basic +public import Mathlib.SetTheory.Cardinal.Cofinality.Ordinal /-! # Club sets @@ -27,7 +25,7 @@ public section universe u v -open Cardinal Order +open Cardinal Order Ordinal /-- A club set is closed under suprema and cofinal. -/ structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where @@ -51,7 +49,7 @@ theorem IsClub.univ : IsClub (α := α) .univ := protected theorem IsClub.nonempty [Nonempty α] (hs : IsClub s) : s.Nonempty := hs.isCofinal.nonempty -theorem _root_.isClub_empty_iff : IsClub (α := α) ∅ ↔ IsEmpty α := +theorem isClub_empty_iff : IsClub (α := α) ∅ ↔ IsEmpty α := ⟨fun h ↦ isCofinal_empty_iff.1 h.isCofinal, fun _ ↦ .of_isEmpty⟩ theorem IsClub.union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) := @@ -127,7 +125,7 @@ theorem IsClub.inter {s t : Set α} (hα : cof α ≠ ℵ₀) (hs : IsClub s) (h rw [← Set.sInter_pair] have H : ∀ x ∈ ({s, t} : Set _), IsClub x := by simpa [hs] obtain hα | hα' := hα.lt_or_gt - · rw [cof_lt_aleph0_iff] at hα + · rw [Order.cof_lt_aleph0_iff] at hα exact .sInter_of_cof_le_one hα H · exact .sInter hα (hα'.trans_le' <| by simp) H @@ -180,7 +178,7 @@ theorem not_isStationary_empty : ¬ IsStationary (∅ : Set α) := by theorem IsClub.isStationary [Nonempty α] [WellFoundedLT α] (hα : cof α ≠ ℵ₀) (hs : IsClub s) : IsStationary s := - fun t ht ↦ (hs.inter hα ht).nonempty + fun _ ht ↦ (hs.inter hα ht).nonempty /-- Non-stationary sets form an ideal. -/ theorem not_isStationary_union [WellFoundedLT α] (hα : cof α ≠ ℵ₀) @@ -191,6 +189,11 @@ theorem not_isStationary_union [WellFoundedLT α] (hα : cof α ≠ ℵ₀) refine ⟨_, hu.inter hα hv, ?_⟩ grind +theorem dirSupClosed_of_type_le_omega0 [WellFoundedLT α] {s : Set α} (hs : typeLT s ≤ ω) : + DirSupClosed s := by + + sorry + theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal (sᶜ)) : IsStationary s := by intro t ht obtain ⟨a, ha⟩ := not_isCofinal_iff.1 hs @@ -199,5 +202,9 @@ theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal (sᶜ)) : IsStati contrapose! ha exact ⟨b, ha, hb'⟩ -proof_wanted isStationary_iff_not_isCofinal_compl (hα : cof α ≤ ℵ₀) : - IsStationary s ↔ ¬ IsCofinal (sᶜ) +theorem isStationary_iff_not_isCofinal_compl [WellFoundedLT α] (hα : cof α ≤ ℵ₀) : + IsStationary s ↔ ¬ IsCofinal (sᶜ) where + mp hs h := by + obtain ⟨t, ht, ht', htα⟩ := Ordinal.ord_cof_eq_of_isCofinal h + sorry + mpr := .of_not_isCofinal_compl diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean index a3fbe3edf236a9..1321006be9bd45 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean @@ -151,7 +151,8 @@ theorem cof_omega0 : cof ω = ℵ₀ := @[deprecated (since := "2026-02-18")] alias cof_eq_one_iff_is_succ := cof_eq_one_iff -theorem ord_cof_eq (α : Type*) [LinearOrder α] [WellFoundedLT α] : +variable (α) in +theorem ord_cof_eq [LinearOrder α] [WellFoundedLT α] : ∃ s : Set α, IsCofinal s ∧ typeLT s = (Order.cof α).ord := by obtain ⟨s, hs, hs'⟩ := Order.cof_eq α obtain ⟨r, hr, hr'⟩ := exists_ord_eq s @@ -166,8 +167,18 @@ theorem ord_cof_eq (α : Type*) [LinearOrder α] [WellFoundedLT α] : · obtain ⟨x, z, hz, rfl⟩ := x exact (hz _ hxy').asymm hxy +theorem ord_cof_eq_of_isCofinal [LinearOrder α] [WellFoundedLT α] {s : Set α} (hs : IsCofinal s) : + ∃ t ⊆ s, IsCofinal t ∧ typeLT t = (Order.cof α).ord := by + obtain ⟨t, ht, ht'⟩ := ord_cof_eq s + rw [cof_eq_of_isCofinal hs] at ht' + refine ⟨t, ?_, hs.trans ht, ?_⟩ + · simp + · rw [← ht'] + exact ((Subtype.strictMono_coe _).strictMonoOn _).orderIso.ordinal_type_eq.symm + +variable (α) in @[simp] -theorem _root_.Order.cof_ord_cof (α : Type*) [LinearOrder α] [WellFoundedLT α] : +theorem _root_.Order.cof_ord_cof [LinearOrder α] [WellFoundedLT α] : (Order.cof α).ord.cof = Order.cof α := by obtain ⟨s, hs, hs'⟩ := ord_cof_eq α rw [← hs', cof_type] @@ -183,6 +194,14 @@ theorem cof_ord_cof (o : Ordinal) : o.cof.ord.cof = o.cof := by @[deprecated (since := "2026-03-21")] alias cof_cof := cof_ord_cof +theorem dirSupClosed_of_type_le_omega0 [LinearOrder α] [WellFoundedLT α] + {s : Set α} (hs : IsCofinal s) (hs' : typeLT s ≤ ω) : DirSupClosed s := by + obtain rfl | hs₀ := s.eq_empty_or_nonempty + · simp + let f (n : ℕ) : α := if hn : n < typeLT s then enum (· < · : s → _) ⟨n, hn⟩ + sorry + +#exit /-! ### Cofinalities and suprema -/ section LinearOrder diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean index e21f2a6560ab15..ad1fb9785be7bd 100644 --- a/Mathlib/SetTheory/Ordinal/Basic.lean +++ b/Mathlib/SetTheory/Ordinal/Basic.lean @@ -169,6 +169,10 @@ theorem _root_.RelIso.ordinal_type_eq {α β} {r : α → α → Prop} {s : β [IsWellOrder β s] (h : r ≃r s) : type r = type s := type_eq.2 ⟨h⟩ +theorem _root_.OrderIso.ordinal_type_eq {α β} [LinearOrder α] [LinearOrder β] + [WellFoundedLT α] [WellFoundedLT β] (h : α ≃o β) : typeLT α = typeLT β := + h.toRelIsoLT.ordinal_type_eq + theorem type_eq_zero_of_empty (r) [IsWellOrder α r] [IsEmpty α] : type r = 0 := (RelIso.relIsoOfIsEmpty r _).ordinal_type_eq From f5ca261aedb794d5a60e34734fdd9137c8313620 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 22 May 2026 16:07:27 -0600 Subject: [PATCH 05/24] finish --- Mathlib/Data/Fintype/Order.lean | 8 ++++++++ Mathlib/Order/DirSupClosed.lean | 26 +++++++++++++++++++++++++- 2 files changed, 33 insertions(+), 1 deletion(-) diff --git a/Mathlib/Data/Fintype/Order.lean b/Mathlib/Data/Fintype/Order.lean index e4a5f7b738f08f..b02781ca86ac7d 100644 --- a/Mathlib/Data/Fintype/Order.lean +++ b/Mathlib/Data/Fintype/Order.lean @@ -195,6 +195,14 @@ lemma Directed.finite_le {ι κ : Sort*} [Nonempty ι] [Finite κ] {f : ι → simpa using (hf.comp_of_surjective PLift.down_surjective).finite_set_le (Set.finite_range (PLift.up ∘ g)) +theorem DirectedOn.finite_le {s : Set α} (hs₀ : s.Nonempty) (D : DirectedOn r s) + (hs : s.Finite) : ∃ z ∈ s, ∀ i ∈ s, r i z := by + have := hs₀.to_subtype + have := hs.to_subtype + obtain ⟨⟨z, hzs⟩, hz⟩ := D.directed_val.finite_le id + use z, hzs + simpa using hz + variable [Nonempty α] [Preorder α] theorem Finite.exists_le [IsDirectedOrder α] (f : β → α) : ∃ M, ∀ i, f i ≤ M := diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean index ead09bf1ac225a..e6401757f06c46 100644 --- a/Mathlib/Order/DirSupClosed.lean +++ b/Mathlib/Order/DirSupClosed.lean @@ -5,11 +5,12 @@ Authors: Christopher Hoskin, Violeta Hernández Palacios -/ module +public import Mathlib.Data.Fintype.Order public import Mathlib.Order.Antisymmetrization public import Mathlib.Order.CompleteLattice.Defs public import Mathlib.Order.UpperLower.Basic -import Mathlib.Data.Set.Lattice +import Mathlib.Data.Nat.Lattice /-! # Sets closed under directed suprema @@ -300,6 +301,29 @@ theorem dirSupClosed_singleton (a : α) : DirSupClosed {a} := by theorem dirSupClosedOn_singleton (a : α) : DirSupClosedOn D {a} := (dirSupClosed_singleton a).dirSupClosedOn +theorem DirSupClosed.of_finite (hs : s.Finite) : DirSupClosed s := by + intro t ht ht₀ ht₁ a ha + obtain ⟨b, hbt, hb⟩ := ht₁.finite_le ht₀ (hs.subset ht) + exact ht <| ha.unique ⟨hb, fun x hx ↦ hx hbt⟩ ▸ hbt + +theorem dirSupClosed_range_nat {f : ℕ → α} (hf : Monotone f) (hf' : IsCofinal (.range f)) : + DirSupClosed (range f) := by + intro s hs hs₀ hs₁ a ha + obtain ⟨_, ⟨n, rfl⟩, han⟩ := hf' a + obtain rfl | han := han.eq_or_lt + · simp + have hfb : BddAbove (f ⁻¹' s) := by + refine ⟨n, fun m hm ↦ ?_⟩ + by_contra! hnm + exact (ha.1 hm).not_gt (han.trans_le (hf hnm.le)) + refine ⟨sSup (f ⁻¹' s), IsLUB.unique ⟨?_, ?_⟩ ha⟩ <;> intro x hx + · obtain ⟨m, rfl⟩ := hs hx + exact hf (le_csSup hfb hx) + · apply hx (Nat.sSup_mem _ hfb) + obtain ⟨x, hx⟩ := hs₀ + obtain ⟨m, rfl⟩ := hs hx + exact ⟨m, hx⟩ + end PartialOrder section LinearOrder From a33cc54cf220965eff573053e427d79346eeea79 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 22 May 2026 16:20:17 -0600 Subject: [PATCH 06/24] add result --- Mathlib/Order/DirSupClosed.lean | 4 ++-- .../Cardinal/Cofinality/Ordinal.lean | 21 +++++++++++++++++-- 2 files changed, 21 insertions(+), 4 deletions(-) diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean index e6401757f06c46..c24c1b613fbea0 100644 --- a/Mathlib/Order/DirSupClosed.lean +++ b/Mathlib/Order/DirSupClosed.lean @@ -289,7 +289,7 @@ lemma dirSupInaccOn_Iic (a : α) : DirSupInaccOn D (Iic a) := end Preorder -namespace PartialOrder +section PartialOrder variable [PartialOrder α] theorem dirSupClosed_singleton (a : α) : DirSupClosed {a} := by @@ -301,7 +301,7 @@ theorem dirSupClosed_singleton (a : α) : DirSupClosed {a} := by theorem dirSupClosedOn_singleton (a : α) : DirSupClosedOn D {a} := (dirSupClosed_singleton a).dirSupClosedOn -theorem DirSupClosed.of_finite (hs : s.Finite) : DirSupClosed s := by +theorem Set.Finite.dirSupClosed (hs : s.Finite) : DirSupClosed s := by intro t ht ht₀ ht₁ a ha obtain ⟨b, hbt, hb⟩ := ht₁.finite_le ht₀ (hs.subset ht) exact ht <| ha.unique ⟨hb, fun x hx ↦ hx hbt⟩ ▸ hbt diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean index a3fbe3edf236a9..655f71e40708ac 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean @@ -151,7 +151,8 @@ theorem cof_omega0 : cof ω = ℵ₀ := @[deprecated (since := "2026-02-18")] alias cof_eq_one_iff_is_succ := cof_eq_one_iff -theorem ord_cof_eq (α : Type*) [LinearOrder α] [WellFoundedLT α] : +variable (α) in +theorem ord_cof_eq [LinearOrder α] [WellFoundedLT α] : ∃ s : Set α, IsCofinal s ∧ typeLT s = (Order.cof α).ord := by obtain ⟨s, hs, hs'⟩ := Order.cof_eq α obtain ⟨r, hr, hr'⟩ := exists_ord_eq s @@ -166,8 +167,9 @@ theorem ord_cof_eq (α : Type*) [LinearOrder α] [WellFoundedLT α] : · obtain ⟨x, z, hz, rfl⟩ := x exact (hz _ hxy').asymm hxy +variable (α) in @[simp] -theorem _root_.Order.cof_ord_cof (α : Type*) [LinearOrder α] [WellFoundedLT α] : +theorem _root_.Order.cof_ord_cof [LinearOrder α] [WellFoundedLT α] : (Order.cof α).ord.cof = Order.cof α := by obtain ⟨s, hs, hs'⟩ := ord_cof_eq α rw [← hs', cof_type] @@ -183,6 +185,21 @@ theorem cof_ord_cof (o : Ordinal) : o.cof.ord.cof = o.cof := by @[deprecated (since := "2026-03-21")] alias cof_cof := cof_ord_cof +theorem dirSupClosed_of_type_le_omega0 [LinearOrder α] [WellFoundedLT α] + {s : Set α} (hs : IsCofinal s) (hω : typeLT s ≤ ω) : DirSupClosed s := by + obtain hω | hω := hω.lt_or_eq + · obtain ⟨n, hn⟩ := lt_omega0.1 hω + apply_fun card at hn + apply Finite.dirSupClosed + rw [Set.Finite, ← mk_lt_aleph0_iff] + simp_all + · let e : ℕ ≃o s := by + rw [omega0, ← lift_id (type _), lift_type_eq] at hω + exact OrderIso.ofRelIsoLT hω.some.symm + have hfs : .range (Subtype.val ∘ e) = s := by simp + rw [← hfs] at hs ⊢ + exact dirSupClosed_range_nat ((Subtype.mono_coe _).comp e.monotone) hs + /-! ### Cofinalities and suprema -/ section LinearOrder From eb59dc0669993f9a7119a917464acda98564dbc4 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 22 May 2026 16:37:30 -0600 Subject: [PATCH 07/24] reduce imports --- Mathlib/Order/DirSupClosed.lean | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean index c24c1b613fbea0..1aa3cb5712e9e8 100644 --- a/Mathlib/Order/DirSupClosed.lean +++ b/Mathlib/Order/DirSupClosed.lean @@ -5,7 +5,7 @@ Authors: Christopher Hoskin, Violeta Hernández Palacios -/ module -public import Mathlib.Data.Fintype.Order +public import Mathlib.Data.Set.Finite.Basic public import Mathlib.Order.Antisymmetrization public import Mathlib.Order.CompleteLattice.Defs public import Mathlib.Order.UpperLower.Basic @@ -292,19 +292,25 @@ end Preorder section PartialOrder variable [PartialOrder α] -theorem dirSupClosed_singleton (a : α) : DirSupClosed {a} := by +theorem DirSupClosed.singleton (a : α) : DirSupClosed {a} := by intro d hda hdn _ b hb rw [hdn.subset_singleton_iff] at hda subst hda exact mem_singleton_of_eq (hb.unique isLUB_singleton) -theorem dirSupClosedOn_singleton (a : α) : DirSupClosedOn D {a} := - (dirSupClosed_singleton a).dirSupClosedOn +@[deprecated (since := "2026-05-22")] alias dirSupClosed_singleton := DirSupClosed.singleton + +theorem DirSupClosedOn.singleton (a : α) : DirSupClosedOn D {a} := + (DirSupClosed.singleton a).dirSupClosedOn + +@[deprecated (since := "2026-05-22")] alias dirSupClosedOn_singleton := DirSupClosedOn.singleton theorem Set.Finite.dirSupClosed (hs : s.Finite) : DirSupClosed s := by - intro t ht ht₀ ht₁ a ha - obtain ⟨b, hbt, hb⟩ := ht₁.finite_le ht₀ (hs.subset ht) - exact ht <| ha.unique ⟨hb, fun x hx ↦ hx hbt⟩ ▸ hbt + induction s, hs using Set.Finite.induction_on with + | empty => exact .empty + | insert has _ hs₁ => + rw [Set.insert_eq] + exact (DirSupClosed.singleton _).union hs₁ theorem dirSupClosed_range_nat {f : ℕ → α} (hf : Monotone f) (hf' : IsCofinal (.range f)) : DirSupClosed (range f) := by From c727a02114dcf4901dcbf43b90fc5453c32951b6 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 22 May 2026 16:51:08 -0600 Subject: [PATCH 08/24] split --- Mathlib.lean | 3 +- Mathlib/Order/DirSupClosed.lean | 376 ------------------ Mathlib/Order/IsNormal.lean | 2 +- .../SetTheory/Cardinal/Cofinality/Club.lean | 2 +- .../Cardinal/Cofinality/Ordinal.lean | 2 + Mathlib/Topology/Order/ScottTopology.lean | 2 +- 6 files changed, 7 insertions(+), 380 deletions(-) delete mode 100644 Mathlib/Order/DirSupClosed.lean diff --git a/Mathlib.lean b/Mathlib.lean index 8b73416360a46f..9e4050acb47e1a 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5914,7 +5914,8 @@ public import Mathlib.Order.Cover public import Mathlib.Order.Defs.LinearOrder public import Mathlib.Order.Defs.PartialOrder public import Mathlib.Order.Defs.Unbundled -public import Mathlib.Order.DirSupClosed +public import Mathlib.Order.DirSupClosed.Basic +public import Mathlib.Order.DirSupClosed.Finite public import Mathlib.Order.Directed public import Mathlib.Order.DirectedInverseSystem public import Mathlib.Order.Disjoint diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean deleted file mode 100644 index 1aa3cb5712e9e8..00000000000000 --- a/Mathlib/Order/DirSupClosed.lean +++ /dev/null @@ -1,376 +0,0 @@ -/- -Copyright (c) 2023 Christopher Hoskin. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Christopher Hoskin, Violeta Hernández Palacios --/ -module - -public import Mathlib.Data.Set.Finite.Basic -public import Mathlib.Order.Antisymmetrization -public import Mathlib.Order.CompleteLattice.Defs -public import Mathlib.Order.UpperLower.Basic - -import Mathlib.Data.Nat.Lattice - -/-! -# Sets closed under directed suprema - -We say that a set `s` is closed under directed suprema whenever it contains all least upper bounds -for nonempty, directed subsets. Conversely, a set `s` is inaccessible by directed suprema whenever -its complement is closed under directed suprema. Equivalently, if the least upper bound of a -nonempty directed set `t` is contained in `s`, then `t` and `s` must have nonempty intersection. - -## Main definitions - -- `DirSupClosed`: sets closed under directed suprema. -- `DirSupInacc`: sets inaccessible by directed suprema. --/ - -@[expose] public section - -variable {α : Type*} {s t : Set α} {D D₁ D₂ : Set (Set α)} - -open Set - -section Preorder -variable [Preorder α] - -/-- A predicate for a set which is closed under directed suprema of nonempty sets. -This is the complement of a `DirSupInaccOn` set. -/ -def DirSupClosedOn (D : Set (Set α)) (s : Set α) : Prop := - ∀ ⦃d⦄, d ∈ D → d ⊆ s → d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → a ∈ s - -/-- A predicate for a set which is inaccessible by directed suprema of nonempty sets in `D`. -This is the complement of a `DirSupClosedOn` set. -/ -def DirSupInaccOn (D : Set (Set α)) (s : Set α) : Prop := - ∀ ⦃d⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty - -/-- A predicate for a set which is closed under directed suprema of nonempty sets. -This is the complement of a `DirSupInacc` set. -/ -def DirSupClosed (s : Set α) : Prop := - ∀ ⦃d⦄, d ⊆ s → d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → a ∈ s - -/-- A predicate for a set which is inaccessible by directed suprema of nonempty sets. -This is the complement of a `DirSupClosed` set. -/ -def DirSupInacc (s : Set α) : Prop := - ∀ ⦃d⦄, d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty - -@[simp] lemma dirSupClosedOn_univ : DirSupClosedOn univ s ↔ DirSupClosed s := by - simp [DirSupClosedOn, DirSupClosed] - -@[simp] lemma dirSupInaccOn_univ : DirSupInaccOn univ s ↔ DirSupInacc s := by - simp [DirSupInaccOn, DirSupInacc] - -@[simp] lemma DirSupClosed.dirSupClosedOn : DirSupClosed s → DirSupClosedOn D s := @fun h _ _ ↦ @h _ -@[simp] lemma DirSupInacc.dirSupInaccOn : DirSupInacc s → DirSupInaccOn D s := @fun h _ _ ↦ @h _ - -@[simp] theorem DirSupClosed.of_isEmpty [IsEmpty α] {s : Set α} : DirSupClosed s := - fun _ _ ⟨a, _⟩ ↦ isEmptyElim a - -@[simp] theorem DirSupInacc.of_isEmpty [IsEmpty α] {s : Set α} : DirSupInacc s := - fun _ ⟨a, _⟩ ↦ isEmptyElim a - -theorem DirSupClosedOn.of_isEmpty [IsEmpty α] {s : Set α} : DirSupClosedOn D s := by simp -theorem DirSupInaccOn.of_isEmpty [IsEmpty α] {s : Set α} : DirSupInaccOn D s := by simp - -@[gcongr] -lemma DirSupClosedOn.mono (hD : D₁ ⊆ D₂) (hf : DirSupClosedOn D₂ s) : DirSupClosedOn D₁ s := - fun _ a ↦ hf (hD a) - -@[gcongr] -lemma DirSupInaccOn.mono (hD : D₁ ⊆ D₂) (hf : DirSupInaccOn D₂ s) : DirSupInaccOn D₁ s := - fun _ a ↦ hf (hD a) - -@[simp] -lemma dirSupClosedOn_compl : DirSupClosedOn D sᶜ ↔ DirSupInaccOn D s := by - simp_rw [DirSupClosedOn, DirSupInaccOn, ← not_disjoint_iff_nonempty_inter] - grind - -@[simp] -lemma dirSupClosed_compl : DirSupClosed sᶜ ↔ DirSupInacc s := by - rw [← dirSupClosedOn_univ, dirSupClosedOn_compl, dirSupInaccOn_univ] - -@[simp] -lemma dirSupInaccOn_compl : DirSupInaccOn D sᶜ ↔ DirSupClosedOn D s := by - rw [← dirSupClosedOn_compl, compl_compl] - -@[simp] -lemma dirSupInacc_compl : DirSupInacc sᶜ ↔ DirSupClosed s := by - rw [← dirSupClosed_compl, compl_compl] - -alias ⟨DirSupInaccOn.of_compl, DirSupInaccOn.compl⟩ := dirSupClosedOn_compl -alias ⟨DirSupClosedOn.of_compl, DirSupClosedOn.compl⟩ := dirSupInaccOn_compl -alias ⟨DirSupInacc.of_compl, DirSupInacc.compl⟩ := dirSupClosed_compl -alias ⟨DirSupClosed.of_compl, DirSupClosed.compl⟩ := dirSupInacc_compl - -@[simp] theorem DirSupClosed.empty : DirSupClosed (∅ : Set α) := by simp [DirSupClosed] -@[simp] theorem DirSupInacc.empty : DirSupInacc (∅ : Set α) := by simp [DirSupInacc] -theorem DirSupClosedOn.empty : DirSupClosedOn D ∅ := by simp -theorem DirSupInaccOn.empty : DirSupInaccOn D ∅ := by simp - -@[simp] theorem DirSupClosed.univ : DirSupClosed (univ : Set α) := by simp [DirSupClosed] -@[simp] theorem DirSupInacc.univ : DirSupInacc (univ : Set α) := by simp [← compl_empty] -theorem DirSupClosedOn.univ : DirSupClosedOn D univ := by simp -theorem DirSupInaccOn.univ : DirSupInaccOn D univ := by simp - -theorem DirSupClosedOn.sInter {s : Set (Set α)} (hs : ∀ x ∈ s, DirSupClosedOn D x) : - DirSupClosedOn D (⋂₀ s) := - fun _d hD hds hd hd' _a ha t ht ↦ hs t ht hD (hds.trans fun _x hx ↦ hx _ ht) hd hd' ha - -theorem DirSupClosed.sInter {s : Set (Set α)} (hs : ∀ x ∈ s, DirSupClosed x) : - DirSupClosed (⋂₀ s) := by - simpa using DirSupClosedOn.sInter fun x hx ↦ (hs x hx).dirSupClosedOn (D := .univ) - -theorem DirSupInaccOn.sUnion {s : Set (Set α)} (hs : ∀ x ∈ s, DirSupInaccOn D x) : - DirSupInaccOn D (⋃₀ s) := by - rw [← dirSupClosedOn_compl, Set.compl_sUnion] - apply DirSupClosedOn.sInter - rintro x ⟨x, hx, rfl⟩ - exact (hs x hx).compl - -theorem DirSupInacc.sUnion {s : Set (Set α)} (hs : ∀ x ∈ s, DirSupInacc x) : - DirSupInacc (⋃₀ s) := by - simpa using DirSupInaccOn.sUnion fun x hx ↦ (hs x hx).dirSupInaccOn (D := .univ) - -theorem DirSupClosedOn.iInter {ι} {f : ι → Set α} (hs : ∀ i, DirSupClosedOn D (f i)) : - DirSupClosedOn D (⋂ i, f i) := by - rw [← sInter_range f] - exact DirSupClosedOn.sInter (by simpa) - -theorem DirSupClosed.iInter {ι} {f : ι → Set α} (hs : ∀ i, DirSupClosed (f i)) : - DirSupClosed (⋂ i, f i) := by - rw [← sInter_range f] - exact DirSupClosed.sInter (by simpa) - -theorem DirSupInaccOn.iUnion {ι} {f : ι → Set α} (hs : ∀ i, DirSupInaccOn D (f i)) : - DirSupInaccOn D (⋃ i, f i) := by - rw [← sUnion_range f] - exact DirSupInaccOn.sUnion (by simpa) - -theorem DirSupInacc.iUnion {ι} {f : ι → Set α} (hs : ∀ i, DirSupInacc (f i)) : - DirSupInacc (⋃ i, f i) := by - rw [← sUnion_range f] - exact DirSupInacc.sUnion (by simpa) - -lemma DirSupClosedOn.inter (hs : DirSupClosedOn D s) (ht : DirSupClosedOn D t) : - DirSupClosedOn D (s ∩ t) := by - rw [← sInter_pair] - refine .sInter ?_ - simpa [hs] - -lemma DirSupClosed.inter (hs : DirSupClosed s) (ht : DirSupClosed t) : DirSupClosed (s ∩ t) := by - simpa using hs.dirSupClosedOn.inter ht.dirSupClosedOn (D := .univ) - -lemma DirSupInaccOn.union (hs : DirSupInaccOn D s) (ht : DirSupInaccOn D t) : - DirSupInaccOn D (s ∪ t) := by - rw [← dirSupClosedOn_compl, compl_union]; exact hs.compl.inter ht.compl - -lemma DirSupInacc.union (hs : DirSupInacc s) (ht : DirSupInacc t) : DirSupInacc (s ∪ t) := by - simpa using hs.dirSupInaccOn.union ht.dirSupInaccOn (D := .univ) - -theorem DirSupClosedOn.union (hDL : IsLowerSet D) - (hs : DirSupClosedOn D s) (ht : DirSupClosedOn D t) : DirSupClosedOn D (s ∪ t) := by - intro d hD hdu hd₀ hd₁ a ha - have hdst : d ∩ s ∪ d ∩ t = d := by grind - rw [← hdst] at hd₀ hd₁ - wlog h : DirectedOn (· ≤ ·) (d ∩ s) ∧ (d ∩ s).Nonempty - · rw [union_comm] at hdu hd₀ hd₁ hdst ⊢ - exact this hDL ht hs hD hdu hd₀ hd₁ ha hdst <| - (directedOn_or_directedOn_of_union' hd₀ hd₁).resolve_right h - obtain ⟨hds, hn⟩ := h - by_cases had : a ∈ lowerBounds (upperBounds (d ∩ s)) - · exact .inl <| hs (hDL inter_subset_left hD) inter_subset_right hn hds - ⟨fun b hb ↦ ha.1 hb.1, had⟩ - · simp only [lowerBounds, mem_setOf_eq, not_forall] at had - obtain ⟨b, hb, hb'⟩ := had - have key : {x ∈ d | ¬ x ≤ b} ⊆ d ∩ t := fun a ⟨had, hab⟩ ↦ - ⟨had, (hdu had).resolve_left fun has ↦ hab <| hb ⟨had, has⟩⟩ - obtain ⟨w, hw⟩ : {x ∈ d | ¬ x ≤ b}.Nonempty := by - contrapose! hb' - apply ha.2 - aesop - refine Or.inr <| ht (hDL inter_subset_left hD) (key.trans inter_subset_right) - ⟨w, hw⟩ (fun x hx y hy ↦ ?_) ?_ - · obtain ⟨z, hz, hz'⟩ := hd₁ _ (.inr (key hx)) _ (.inr (key hy)) - exact ⟨z, ⟨⟨hdst ▸ hz, mt hz'.1.trans hx.2⟩, hz'⟩⟩ - · refine ⟨fun x hx ↦ ha.1 hx.1, fun x hx ↦ ha.2 fun y hy ↦ ?_⟩ - by_cases hyb : y ≤ b - · obtain ⟨z, hz, hxz, hyz⟩ := hd₁ _ (hdst ▸ hy) _ (.inr (key hw)) - exact hxz.trans (hx ⟨hdst ▸ hz, fun hzb ↦ hw.2 (hyz.trans hzb)⟩) - exact hx ⟨hy, hyb⟩ - -theorem DirSupInaccOn.inter (hDL : IsLowerSet D) - (hs : DirSupInaccOn D s) (ht : DirSupInaccOn D t) : DirSupInaccOn D (s ∩ t) := by - rw [← dirSupClosedOn_compl, compl_inter]; exact hs.compl.union hDL ht.compl - -theorem DirSupClosed.union (hs : DirSupClosed s) (ht : DirSupClosed t) : DirSupClosed (s ∪ t) := by - simpa using hs.dirSupClosedOn.union isLowerSet_univ ht.dirSupClosedOn - -theorem DirSupInacc.inter (hs : DirSupInacc s) (ht : DirSupInacc t) : DirSupInacc (s ∩ t) := by - simpa using hs.dirSupInaccOn.inter isLowerSet_univ ht.dirSupInaccOn - -theorem DirSupInaccOn.of_inter_subset - (h : ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d → - ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s) : DirSupInaccOn D s := by - intro d hd₀ hd₁ hd₂ a hda hd₃ - obtain ⟨b, hbd, hb⟩ := h hd₀ hd₁ hd₂ hda hd₃ - exact ⟨b, hbd, hb ⟨le_rfl, hbd⟩⟩ - -theorem DirSupInacc.of_inter_subset - (h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (· ≤ ·) d → - ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s) : DirSupInacc s := - dirSupInaccOn_univ.1 (.of_inter_subset (by simpa)) - -/-- The condition `(d ∩ s).Nonempty` in `DirSupInaccOn` can be replaced with the stronger -`∃ b ∈ d, Ici b ∩ d ⊆ s` (under mild assumptions on `D`). -/ -theorem dirSupInaccOn_iff_inter_subset (hDL : IsLowerSet D) : - DirSupInaccOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d → - ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s where - mpr := .of_inter_subset - mp h t hD ht₀ ht₁ a ha has := by - by_contra! H - have H : ∀ b : t, ∃ c, b.1 ≤ c ∧ c ∈ t ∧ c ∉ s := by simpa [not_subset, and_assoc] using H - choose f hf using H - have := ht₀.to_subtype - have hft : range f ⊆ t := by grind - apply (h (hDL hft hD) (range_nonempty f) _ _ has).ne_empty - · aesop - · intro a ha b hb - obtain ⟨c, hc, _, _⟩ := ht₁ _ (hft ha) _ (hft hb) - have := hf ⟨c, hc⟩ - grind - · exact ⟨upperBounds_mono_set hft ha.1, - fun b hb ↦ ha.2 fun c hc ↦ (hf ⟨c, hc⟩).1.trans (hb <| by simp)⟩ - -/-- The condition `(d ∩ s).Nonempty` in `DirSupInacc` can be replaced with the stronger -`∃ b ∈ d, Ici b ∩ d ⊆ s`. -/ -theorem dirSupInacc_iff_inter_subset : - DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (· ≤ ·) d → - ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s := by - simpa using dirSupInaccOn_iff_inter_subset isLowerSet_univ - -lemma IsUpperSet.dirSupClosed (hs : IsUpperSet s) : DirSupClosed s := - fun _d hds ⟨_b, hb⟩ _ _a ha ↦ hs (ha.1 hb) <| hds hb - -lemma IsUpperSet.dirSupClosedOn (hs : IsUpperSet s) : DirSupClosedOn D s := - hs.dirSupClosed.dirSupClosedOn - -lemma IsLowerSet.dirSupInacc (hs : IsLowerSet s) : DirSupInacc s := - .of_compl hs.compl.dirSupClosed - -lemma IsLowerSet.dirSupInaccOn (hs : IsLowerSet s) : DirSupInaccOn D s := - .of_compl hs.compl.dirSupClosedOn - -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 - -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 dirSupClosed_Iic (a : α) : DirSupClosed (Iic a) := - fun _d h _ _ _a ha ↦ (isLUB_le_iff ha).2 h - -lemma dirSupClosedOn_Iic (a : α) : DirSupClosedOn D (Iic a) := - (dirSupClosed_Iic a).dirSupClosedOn - -lemma dirSupInacc_Iic (a : α) : DirSupInacc (Iic a) := - (isLowerSet_Iic a).dirSupInacc - -lemma dirSupInaccOn_Iic (a : α) : DirSupInaccOn D (Iic a) := - (isLowerSet_Iic a).dirSupInaccOn - -end Preorder - -section PartialOrder -variable [PartialOrder α] - -theorem DirSupClosed.singleton (a : α) : DirSupClosed {a} := by - intro d hda hdn _ b hb - rw [hdn.subset_singleton_iff] at hda - subst hda - exact mem_singleton_of_eq (hb.unique isLUB_singleton) - -@[deprecated (since := "2026-05-22")] alias dirSupClosed_singleton := DirSupClosed.singleton - -theorem DirSupClosedOn.singleton (a : α) : DirSupClosedOn D {a} := - (DirSupClosed.singleton a).dirSupClosedOn - -@[deprecated (since := "2026-05-22")] alias dirSupClosedOn_singleton := DirSupClosedOn.singleton - -theorem Set.Finite.dirSupClosed (hs : s.Finite) : DirSupClosed s := by - induction s, hs using Set.Finite.induction_on with - | empty => exact .empty - | insert has _ hs₁ => - rw [Set.insert_eq] - exact (DirSupClosed.singleton _).union hs₁ - -theorem dirSupClosed_range_nat {f : ℕ → α} (hf : Monotone f) (hf' : IsCofinal (.range f)) : - DirSupClosed (range f) := by - intro s hs hs₀ hs₁ a ha - obtain ⟨_, ⟨n, rfl⟩, han⟩ := hf' a - obtain rfl | han := han.eq_or_lt - · simp - have hfb : BddAbove (f ⁻¹' s) := by - refine ⟨n, fun m hm ↦ ?_⟩ - by_contra! hnm - exact (ha.1 hm).not_gt (han.trans_le (hf hnm.le)) - refine ⟨sSup (f ⁻¹' s), IsLUB.unique ⟨?_, ?_⟩ ha⟩ <;> intro x hx - · obtain ⟨m, rfl⟩ := hs hx - exact hf (le_csSup hfb hx) - · apply hx (Nat.sSup_mem _ hfb) - obtain ⟨x, hx⟩ := hs₀ - obtain ⟨m, rfl⟩ := hs hx - exact ⟨m, hx⟩ - -end PartialOrder - -section LinearOrder -variable [LinearOrder α] - -theorem dirSupClosedOn_iff_of_linearOrder : - DirSupClosedOn D s ↔ ∀ ⦃d⦄, d ∈ D → d ⊆ s → d.Nonempty → ∀ ⦃a⦄, IsLUB d a → a ∈ s := by - simp [DirSupClosedOn] - -theorem dirSupClosed_iff_of_linearOrder : - DirSupClosed s ↔ ∀ ⦃d⦄, d ⊆ s → d.Nonempty → ∀ ⦃a⦄, IsLUB d a → a ∈ s := by - simp [DirSupClosed] - -theorem dirSupInaccOn_iff_of_linearOrder : - DirSupInaccOn D s ↔ - ∀ ⦃d⦄, d ∈ D → d.Nonempty → ∀ ⦃a⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty := by - simp [DirSupInaccOn] - -theorem dirSupInacc_iff_of_linearOrder : - DirSupInacc s ↔ ∀ ⦃d⦄, d.Nonempty → ∀ ⦃a⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty := by - simp [DirSupInacc] - -end LinearOrder - -section CompleteLattice -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 - 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 - simp [DirSupInacc, isLUB_iff_sSup_eq] - -end CompleteLattice diff --git a/Mathlib/Order/IsNormal.lean b/Mathlib/Order/IsNormal.lean index df523f0f92b52c..ab3270cd436568 100644 --- a/Mathlib/Order/IsNormal.lean +++ b/Mathlib/Order/IsNormal.lean @@ -6,7 +6,7 @@ Authors: Violeta Hernández Palacios module public import Mathlib.Dynamics.FixedPoints.Defs -public import Mathlib.Order.DirSupClosed +public import Mathlib.Order.DirSupClosed.Basic public import Mathlib.Order.SuccPred.CompleteLinearOrder public import Mathlib.Order.SuccPred.InitialSeg diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index 58671ac506a2db..bb72fb8f966a10 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -5,7 +5,7 @@ Authors: Violeta Hernández Palacios -/ module -public import Mathlib.Order.DirSupClosed +public import Mathlib.Order.DirSupClosed.Basic public import Mathlib.Order.IsNormal public import Mathlib.SetTheory.Cardinal.Cofinality.Basic diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean index 655f71e40708ac..426f4876135e0f 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean @@ -9,6 +9,8 @@ public import Mathlib.SetTheory.Cardinal.Arithmetic public import Mathlib.SetTheory.Cardinal.Cofinality.Basic public import Mathlib.SetTheory.Ordinal.FixedPoint +import Mathlib.Order.DirSupClosed.Finite + /-! # Cofinality of an ordinal diff --git a/Mathlib/Topology/Order/ScottTopology.lean b/Mathlib/Topology/Order/ScottTopology.lean index 8e996159cb0c82..1e1d522fd229f0 100644 --- a/Mathlib/Topology/Order/ScottTopology.lean +++ b/Mathlib/Topology/Order/ScottTopology.lean @@ -5,7 +5,7 @@ Authors: Christopher Hoskin -/ module -public import Mathlib.Order.DirSupClosed +public import Mathlib.Order.DirSupClosed.Basic public import Mathlib.Order.ScottContinuity public import Mathlib.Topology.Order.UpperLowerSetTopology From 8d9e99f2266a5c846fd06e99c746d6ffee6e6c6e Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 22 May 2026 16:51:13 -0600 Subject: [PATCH 09/24] split --- Mathlib/Order/DirSupClosed/Basic.lean | 350 +++++++++++++++++++++++++ Mathlib/Order/DirSupClosed/Finite.lean | 44 ++++ 2 files changed, 394 insertions(+) create mode 100644 Mathlib/Order/DirSupClosed/Basic.lean create mode 100644 Mathlib/Order/DirSupClosed/Finite.lean diff --git a/Mathlib/Order/DirSupClosed/Basic.lean b/Mathlib/Order/DirSupClosed/Basic.lean new file mode 100644 index 00000000000000..9816253c8526c3 --- /dev/null +++ b/Mathlib/Order/DirSupClosed/Basic.lean @@ -0,0 +1,350 @@ +/- +Copyright (c) 2023 Christopher Hoskin. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +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 + +import Mathlib.Data.Set.Lattice + +/-! +# Sets closed under directed suprema + +We say that a set `s` is closed under directed suprema whenever it contains all least upper bounds +for nonempty, directed subsets. Conversely, a set `s` is inaccessible by directed suprema whenever +its complement is closed under directed suprema. Equivalently, if the least upper bound of a +nonempty directed set `t` is contained in `s`, then `t` and `s` must have nonempty intersection. + +## Main definitions + +- `DirSupClosed`: sets closed under directed suprema. +- `DirSupInacc`: sets inaccessible by directed suprema. +-/ + +@[expose] public section + +variable {α : Type*} {s t : Set α} {D D₁ D₂ : Set (Set α)} + +open Set + +section Preorder +variable [Preorder α] + +/-- A predicate for a set which is closed under directed suprema of nonempty sets. +This is the complement of a `DirSupInaccOn` set. -/ +def DirSupClosedOn (D : Set (Set α)) (s : Set α) : Prop := + ∀ ⦃d⦄, d ∈ D → d ⊆ s → d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → a ∈ s + +/-- A predicate for a set which is inaccessible by directed suprema of nonempty sets in `D`. +This is the complement of a `DirSupClosedOn` set. -/ +def DirSupInaccOn (D : Set (Set α)) (s : Set α) : Prop := + ∀ ⦃d⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty + +/-- A predicate for a set which is closed under directed suprema of nonempty sets. +This is the complement of a `DirSupInacc` set. -/ +def DirSupClosed (s : Set α) : Prop := + ∀ ⦃d⦄, d ⊆ s → d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → a ∈ s + +/-- A predicate for a set which is inaccessible by directed suprema of nonempty sets. +This is the complement of a `DirSupClosed` set. -/ +def DirSupInacc (s : Set α) : Prop := + ∀ ⦃d⦄, d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty + +@[simp] lemma dirSupClosedOn_univ : DirSupClosedOn univ s ↔ DirSupClosed s := by + simp [DirSupClosedOn, DirSupClosed] + +@[simp] lemma dirSupInaccOn_univ : DirSupInaccOn univ s ↔ DirSupInacc s := by + simp [DirSupInaccOn, DirSupInacc] + +@[simp] lemma DirSupClosed.dirSupClosedOn : DirSupClosed s → DirSupClosedOn D s := @fun h _ _ ↦ @h _ +@[simp] lemma DirSupInacc.dirSupInaccOn : DirSupInacc s → DirSupInaccOn D s := @fun h _ _ ↦ @h _ + +@[simp] theorem DirSupClosed.of_isEmpty [IsEmpty α] {s : Set α} : DirSupClosed s := + fun _ _ ⟨a, _⟩ ↦ isEmptyElim a + +@[simp] theorem DirSupInacc.of_isEmpty [IsEmpty α] {s : Set α} : DirSupInacc s := + fun _ ⟨a, _⟩ ↦ isEmptyElim a + +theorem DirSupClosedOn.of_isEmpty [IsEmpty α] {s : Set α} : DirSupClosedOn D s := by simp +theorem DirSupInaccOn.of_isEmpty [IsEmpty α] {s : Set α} : DirSupInaccOn D s := by simp + +@[gcongr] +lemma DirSupClosedOn.mono (hD : D₁ ⊆ D₂) (hf : DirSupClosedOn D₂ s) : DirSupClosedOn D₁ s := + fun _ a ↦ hf (hD a) + +@[gcongr] +lemma DirSupInaccOn.mono (hD : D₁ ⊆ D₂) (hf : DirSupInaccOn D₂ s) : DirSupInaccOn D₁ s := + fun _ a ↦ hf (hD a) + +@[simp] +lemma dirSupClosedOn_compl : DirSupClosedOn D sᶜ ↔ DirSupInaccOn D s := by + simp_rw [DirSupClosedOn, DirSupInaccOn, ← not_disjoint_iff_nonempty_inter] + grind + +@[simp] +lemma dirSupClosed_compl : DirSupClosed sᶜ ↔ DirSupInacc s := by + rw [← dirSupClosedOn_univ, dirSupClosedOn_compl, dirSupInaccOn_univ] + +@[simp] +lemma dirSupInaccOn_compl : DirSupInaccOn D sᶜ ↔ DirSupClosedOn D s := by + rw [← dirSupClosedOn_compl, compl_compl] + +@[simp] +lemma dirSupInacc_compl : DirSupInacc sᶜ ↔ DirSupClosed s := by + rw [← dirSupClosed_compl, compl_compl] + +alias ⟨DirSupInaccOn.of_compl, DirSupInaccOn.compl⟩ := dirSupClosedOn_compl +alias ⟨DirSupClosedOn.of_compl, DirSupClosedOn.compl⟩ := dirSupInaccOn_compl +alias ⟨DirSupInacc.of_compl, DirSupInacc.compl⟩ := dirSupClosed_compl +alias ⟨DirSupClosed.of_compl, DirSupClosed.compl⟩ := dirSupInacc_compl + +@[simp] theorem DirSupClosed.empty : DirSupClosed (∅ : Set α) := by simp [DirSupClosed] +@[simp] theorem DirSupInacc.empty : DirSupInacc (∅ : Set α) := by simp [DirSupInacc] +theorem DirSupClosedOn.empty : DirSupClosedOn D ∅ := by simp +theorem DirSupInaccOn.empty : DirSupInaccOn D ∅ := by simp + +@[simp] theorem DirSupClosed.univ : DirSupClosed (univ : Set α) := by simp [DirSupClosed] +@[simp] theorem DirSupInacc.univ : DirSupInacc (univ : Set α) := by simp [← compl_empty] +theorem DirSupClosedOn.univ : DirSupClosedOn D univ := by simp +theorem DirSupInaccOn.univ : DirSupInaccOn D univ := by simp + +theorem DirSupClosedOn.sInter {s : Set (Set α)} (hs : ∀ x ∈ s, DirSupClosedOn D x) : + DirSupClosedOn D (⋂₀ s) := + fun _d hD hds hd hd' _a ha t ht ↦ hs t ht hD (hds.trans fun _x hx ↦ hx _ ht) hd hd' ha + +theorem DirSupClosed.sInter {s : Set (Set α)} (hs : ∀ x ∈ s, DirSupClosed x) : + DirSupClosed (⋂₀ s) := by + simpa using DirSupClosedOn.sInter fun x hx ↦ (hs x hx).dirSupClosedOn (D := .univ) + +theorem DirSupInaccOn.sUnion {s : Set (Set α)} (hs : ∀ x ∈ s, DirSupInaccOn D x) : + DirSupInaccOn D (⋃₀ s) := by + rw [← dirSupClosedOn_compl, Set.compl_sUnion] + apply DirSupClosedOn.sInter + rintro x ⟨x, hx, rfl⟩ + exact (hs x hx).compl + +theorem DirSupInacc.sUnion {s : Set (Set α)} (hs : ∀ x ∈ s, DirSupInacc x) : + DirSupInacc (⋃₀ s) := by + simpa using DirSupInaccOn.sUnion fun x hx ↦ (hs x hx).dirSupInaccOn (D := .univ) + +theorem DirSupClosedOn.iInter {ι} {f : ι → Set α} (hs : ∀ i, DirSupClosedOn D (f i)) : + DirSupClosedOn D (⋂ i, f i) := by + rw [← sInter_range f] + exact DirSupClosedOn.sInter (by simpa) + +theorem DirSupClosed.iInter {ι} {f : ι → Set α} (hs : ∀ i, DirSupClosed (f i)) : + DirSupClosed (⋂ i, f i) := by + rw [← sInter_range f] + exact DirSupClosed.sInter (by simpa) + +theorem DirSupInaccOn.iUnion {ι} {f : ι → Set α} (hs : ∀ i, DirSupInaccOn D (f i)) : + DirSupInaccOn D (⋃ i, f i) := by + rw [← sUnion_range f] + exact DirSupInaccOn.sUnion (by simpa) + +theorem DirSupInacc.iUnion {ι} {f : ι → Set α} (hs : ∀ i, DirSupInacc (f i)) : + DirSupInacc (⋃ i, f i) := by + rw [← sUnion_range f] + exact DirSupInacc.sUnion (by simpa) + +lemma DirSupClosedOn.inter (hs : DirSupClosedOn D s) (ht : DirSupClosedOn D t) : + DirSupClosedOn D (s ∩ t) := by + rw [← sInter_pair] + refine .sInter ?_ + simpa [hs] + +lemma DirSupClosed.inter (hs : DirSupClosed s) (ht : DirSupClosed t) : DirSupClosed (s ∩ t) := by + simpa using hs.dirSupClosedOn.inter ht.dirSupClosedOn (D := .univ) + +lemma DirSupInaccOn.union (hs : DirSupInaccOn D s) (ht : DirSupInaccOn D t) : + DirSupInaccOn D (s ∪ t) := by + rw [← dirSupClosedOn_compl, compl_union]; exact hs.compl.inter ht.compl + +lemma DirSupInacc.union (hs : DirSupInacc s) (ht : DirSupInacc t) : DirSupInacc (s ∪ t) := by + simpa using hs.dirSupInaccOn.union ht.dirSupInaccOn (D := .univ) + +theorem DirSupClosedOn.union (hDL : IsLowerSet D) + (hs : DirSupClosedOn D s) (ht : DirSupClosedOn D t) : DirSupClosedOn D (s ∪ t) := by + intro d hD hdu hd₀ hd₁ a ha + have hdst : d ∩ s ∪ d ∩ t = d := by grind + rw [← hdst] at hd₀ hd₁ + wlog h : DirectedOn (· ≤ ·) (d ∩ s) ∧ (d ∩ s).Nonempty + · rw [union_comm] at hdu hd₀ hd₁ hdst ⊢ + exact this hDL ht hs hD hdu hd₀ hd₁ ha hdst <| + (directedOn_or_directedOn_of_union' hd₀ hd₁).resolve_right h + obtain ⟨hds, hn⟩ := h + by_cases had : a ∈ lowerBounds (upperBounds (d ∩ s)) + · exact .inl <| hs (hDL inter_subset_left hD) inter_subset_right hn hds + ⟨fun b hb ↦ ha.1 hb.1, had⟩ + · simp only [lowerBounds, mem_setOf_eq, not_forall] at had + obtain ⟨b, hb, hb'⟩ := had + have key : {x ∈ d | ¬ x ≤ b} ⊆ d ∩ t := fun a ⟨had, hab⟩ ↦ + ⟨had, (hdu had).resolve_left fun has ↦ hab <| hb ⟨had, has⟩⟩ + obtain ⟨w, hw⟩ : {x ∈ d | ¬ x ≤ b}.Nonempty := by + contrapose! hb' + apply ha.2 + aesop + refine Or.inr <| ht (hDL inter_subset_left hD) (key.trans inter_subset_right) + ⟨w, hw⟩ (fun x hx y hy ↦ ?_) ?_ + · obtain ⟨z, hz, hz'⟩ := hd₁ _ (.inr (key hx)) _ (.inr (key hy)) + exact ⟨z, ⟨⟨hdst ▸ hz, mt hz'.1.trans hx.2⟩, hz'⟩⟩ + · refine ⟨fun x hx ↦ ha.1 hx.1, fun x hx ↦ ha.2 fun y hy ↦ ?_⟩ + by_cases hyb : y ≤ b + · obtain ⟨z, hz, hxz, hyz⟩ := hd₁ _ (hdst ▸ hy) _ (.inr (key hw)) + exact hxz.trans (hx ⟨hdst ▸ hz, fun hzb ↦ hw.2 (hyz.trans hzb)⟩) + exact hx ⟨hy, hyb⟩ + +theorem DirSupInaccOn.inter (hDL : IsLowerSet D) + (hs : DirSupInaccOn D s) (ht : DirSupInaccOn D t) : DirSupInaccOn D (s ∩ t) := by + rw [← dirSupClosedOn_compl, compl_inter]; exact hs.compl.union hDL ht.compl + +theorem DirSupClosed.union (hs : DirSupClosed s) (ht : DirSupClosed t) : DirSupClosed (s ∪ t) := by + simpa using hs.dirSupClosedOn.union isLowerSet_univ ht.dirSupClosedOn + +theorem DirSupInacc.inter (hs : DirSupInacc s) (ht : DirSupInacc t) : DirSupInacc (s ∩ t) := by + simpa using hs.dirSupInaccOn.inter isLowerSet_univ ht.dirSupInaccOn + +theorem DirSupInaccOn.of_inter_subset + (h : ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d → + ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s) : DirSupInaccOn D s := by + intro d hd₀ hd₁ hd₂ a hda hd₃ + obtain ⟨b, hbd, hb⟩ := h hd₀ hd₁ hd₂ hda hd₃ + exact ⟨b, hbd, hb ⟨le_rfl, hbd⟩⟩ + +theorem DirSupInacc.of_inter_subset + (h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (· ≤ ·) d → + ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s) : DirSupInacc s := + dirSupInaccOn_univ.1 (.of_inter_subset (by simpa)) + +/-- The condition `(d ∩ s).Nonempty` in `DirSupInaccOn` can be replaced with the stronger +`∃ b ∈ d, Ici b ∩ d ⊆ s` (under mild assumptions on `D`). -/ +theorem dirSupInaccOn_iff_inter_subset (hDL : IsLowerSet D) : + DirSupInaccOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d → + ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s where + mpr := .of_inter_subset + mp h t hD ht₀ ht₁ a ha has := by + by_contra! H + have H : ∀ b : t, ∃ c, b.1 ≤ c ∧ c ∈ t ∧ c ∉ s := by simpa [not_subset, and_assoc] using H + choose f hf using H + have := ht₀.to_subtype + have hft : range f ⊆ t := by grind + apply (h (hDL hft hD) (range_nonempty f) _ _ has).ne_empty + · aesop + · intro a ha b hb + obtain ⟨c, hc, _, _⟩ := ht₁ _ (hft ha) _ (hft hb) + have := hf ⟨c, hc⟩ + grind + · exact ⟨upperBounds_mono_set hft ha.1, + fun b hb ↦ ha.2 fun c hc ↦ (hf ⟨c, hc⟩).1.trans (hb <| by simp)⟩ + +/-- The condition `(d ∩ s).Nonempty` in `DirSupInacc` can be replaced with the stronger +`∃ b ∈ d, Ici b ∩ d ⊆ s`. -/ +theorem dirSupInacc_iff_inter_subset : + DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (· ≤ ·) d → + ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s := by + simpa using dirSupInaccOn_iff_inter_subset isLowerSet_univ + +lemma IsUpperSet.dirSupClosed (hs : IsUpperSet s) : DirSupClosed s := + fun _d hds ⟨_b, hb⟩ _ _a ha ↦ hs (ha.1 hb) <| hds hb + +lemma IsUpperSet.dirSupClosedOn (hs : IsUpperSet s) : DirSupClosedOn D s := + hs.dirSupClosed.dirSupClosedOn + +lemma IsLowerSet.dirSupInacc (hs : IsLowerSet s) : DirSupInacc s := + .of_compl hs.compl.dirSupClosed + +lemma IsLowerSet.dirSupInaccOn (hs : IsLowerSet s) : DirSupInaccOn D s := + .of_compl hs.compl.dirSupClosedOn + +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 + +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 dirSupClosed_Iic (a : α) : DirSupClosed (Iic a) := + fun _d h _ _ _a ha ↦ (isLUB_le_iff ha).2 h + +lemma dirSupClosedOn_Iic (a : α) : DirSupClosedOn D (Iic a) := + (dirSupClosed_Iic a).dirSupClosedOn + +lemma dirSupInacc_Iic (a : α) : DirSupInacc (Iic a) := + (isLowerSet_Iic a).dirSupInacc + +lemma dirSupInaccOn_Iic (a : α) : DirSupInaccOn D (Iic a) := + (isLowerSet_Iic a).dirSupInaccOn + +end Preorder + +section PartialOrder +variable [PartialOrder α] + +theorem DirSupClosed.singleton (a : α) : DirSupClosed {a} := by + intro d hda hdn _ b hb + rw [hdn.subset_singleton_iff] at hda + subst hda + exact mem_singleton_of_eq (hb.unique isLUB_singleton) + +@[deprecated (since := "2026-05-22")] alias dirSupClosed_singleton := DirSupClosed.singleton + +theorem DirSupClosedOn.singleton (a : α) : DirSupClosedOn D {a} := + (DirSupClosed.singleton a).dirSupClosedOn + +@[deprecated (since := "2026-05-22")] alias dirSupClosedOn_singleton := DirSupClosedOn.singleton + +end PartialOrder + +section LinearOrder +variable [LinearOrder α] + +theorem dirSupClosedOn_iff_of_linearOrder : + DirSupClosedOn D s ↔ ∀ ⦃d⦄, d ∈ D → d ⊆ s → d.Nonempty → ∀ ⦃a⦄, IsLUB d a → a ∈ s := by + simp [DirSupClosedOn] + +theorem dirSupClosed_iff_of_linearOrder : + DirSupClosed s ↔ ∀ ⦃d⦄, d ⊆ s → d.Nonempty → ∀ ⦃a⦄, IsLUB d a → a ∈ s := by + simp [DirSupClosed] + +theorem dirSupInaccOn_iff_of_linearOrder : + DirSupInaccOn D s ↔ + ∀ ⦃d⦄, d ∈ D → d.Nonempty → ∀ ⦃a⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty := by + simp [DirSupInaccOn] + +theorem dirSupInacc_iff_of_linearOrder : + DirSupInacc s ↔ ∀ ⦃d⦄, d.Nonempty → ∀ ⦃a⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty := by + simp [DirSupInacc] + +end LinearOrder + +section CompleteLattice +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 + 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 + simp [DirSupInacc, isLUB_iff_sSup_eq] + +end CompleteLattice diff --git a/Mathlib/Order/DirSupClosed/Finite.lean b/Mathlib/Order/DirSupClosed/Finite.lean new file mode 100644 index 00000000000000..94661c1032c5c9 --- /dev/null +++ b/Mathlib/Order/DirSupClosed/Finite.lean @@ -0,0 +1,44 @@ +/- +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.Data.Set.Finite.Basic +public import Mathlib.Order.DirSupClosed.Basic + +import Mathlib.Data.Nat.Lattice + +/-! +# Finite sets are closed under suprema +-/ + +public section + +variable {α : Type*} [PartialOrder α] + +theorem Set.Finite.dirSupClosed {s : Set α} (hs : s.Finite) : DirSupClosed s := by + induction s, hs using Set.Finite.induction_on with + | empty => exact .empty + | insert has _ hs₁ => + rw [Set.insert_eq] + exact (DirSupClosed.singleton _).union hs₁ + +theorem dirSupClosed_range_nat {f : ℕ → α} (hf : Monotone f) (hf' : IsCofinal (.range f)) : + DirSupClosed (.range f) := by + intro s hs hs₀ hs₁ a ha + obtain ⟨_, ⟨n, rfl⟩, han⟩ := hf' a + obtain rfl | han := han.eq_or_lt + · simp + have hfb : BddAbove (f ⁻¹' s) := by + refine ⟨n, fun m hm ↦ ?_⟩ + by_contra! hnm + exact (ha.1 hm).not_gt (han.trans_le (hf hnm.le)) + refine ⟨sSup (f ⁻¹' s), IsLUB.unique ⟨?_, ?_⟩ ha⟩ <;> intro x hx + · obtain ⟨m, rfl⟩ := hs hx + exact hf (le_csSup hfb hx) + · apply hx (Nat.sSup_mem _ hfb) + obtain ⟨x, hx⟩ := hs₀ + obtain ⟨m, rfl⟩ := hs hx + exact ⟨m, hx⟩ From 84e1e9b0a2e9ff793918881001573e83c70be1cd Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 22 May 2026 16:51:44 -0600 Subject: [PATCH 10/24] golf --- Mathlib/Order/DirSupClosed/Finite.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Order/DirSupClosed/Finite.lean b/Mathlib/Order/DirSupClosed/Finite.lean index 94661c1032c5c9..84a2fb4650b209 100644 --- a/Mathlib/Order/DirSupClosed/Finite.lean +++ b/Mathlib/Order/DirSupClosed/Finite.lean @@ -19,7 +19,7 @@ public section variable {α : Type*} [PartialOrder α] theorem Set.Finite.dirSupClosed {s : Set α} (hs : s.Finite) : DirSupClosed s := by - induction s, hs using Set.Finite.induction_on with + induction s, hs using induction_on with | empty => exact .empty | insert has _ hs₁ => rw [Set.insert_eq] From 1e4865ec2e580c137d7b86d8702d780abbc3cac8 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 22 May 2026 16:53:29 -0600 Subject: [PATCH 11/24] have --- Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean index 426f4876135e0f..7a0d660c34b13b 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean @@ -195,7 +195,7 @@ theorem dirSupClosed_of_type_le_omega0 [LinearOrder α] [WellFoundedLT α] apply Finite.dirSupClosed rw [Set.Finite, ← mk_lt_aleph0_iff] simp_all - · let e : ℕ ≃o s := by + · have e : ℕ ≃o s := by rw [omega0, ← lift_id (type _), lift_type_eq] at hω exact OrderIso.ofRelIsoLT hω.some.symm have hfs : .range (Subtype.val ∘ e) = s := by simp From 415ba668c090f080bf55d3449e7fb2423f44b1a7 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 22 May 2026 17:04:09 -0600 Subject: [PATCH 12/24] start --- .../SetTheory/Cardinal/Cofinality/Club.lean | 72 +++++++++++++++++-- 1 file changed, 67 insertions(+), 5 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index 58671ac506a2db..e2efa682bbd307 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -5,9 +5,7 @@ Authors: Violeta Hernández Palacios -/ module -public import Mathlib.Order.DirSupClosed -public import Mathlib.Order.IsNormal -public import Mathlib.SetTheory.Cardinal.Cofinality.Basic +public import Mathlib.SetTheory.Cardinal.Cofinality.Ordinal /-! # Club sets @@ -27,7 +25,7 @@ public section universe u v -open Cardinal Order +open Cardinal Order Ordinal /-- A club set is closed under suprema and cofinal. -/ structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where @@ -48,6 +46,12 @@ theorem IsClub.of_isEmpty [IsEmpty α] {s : Set α} : IsClub s := theorem IsClub.univ : IsClub (α := α) .univ := ⟨.univ, .univ⟩ +protected theorem IsClub.nonempty [Nonempty α] (hs : IsClub s) : s.Nonempty := + hs.isCofinal.nonempty + +theorem isClub_empty_iff : IsClub (α := α) ∅ ↔ IsEmpty α := + ⟨fun h ↦ isCofinal_empty_iff.1 h.isCofinal, fun _ ↦ .of_isEmpty⟩ + theorem IsClub.union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) := ⟨hs.dirSupClosed.union ht.dirSupClosed, hs.isCofinal.mono Set.subset_union_left⟩ @@ -121,7 +125,7 @@ theorem IsClub.inter {s t : Set α} (hα : cof α ≠ ℵ₀) (hs : IsClub s) (h rw [← Set.sInter_pair] have H : ∀ x ∈ ({s, t} : Set _), IsClub x := by simpa [hs] obtain hα | hα' := hα.lt_or_gt - · rw [cof_lt_aleph0_iff] at hα + · rw [Order.cof_lt_aleph0_iff] at hα exact .sInter_of_cof_le_one hα H · exact .sInter hα (hα'.trans_le' <| by simp) H @@ -144,3 +148,61 @@ theorem Order.IsNormal.isClub_fixedPoints {f : α → α} (hα : cof α ≠ ℵ 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. -/ +@[expose] +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 [IsStationary, ← not_imp_not (b := IsClub _), Set.not_nonempty_iff_eq_empty, + isClub_empty_iff] + +@[simp] +theorem IsStationary.univ [Nonempty α] : IsStationary (.univ (α := α)) := + isStationary_univ_iff.2 ‹_› + +@[simp] +theorem not_isStationary_empty : ¬ IsStationary (∅ : Set α) := by + intro h + simpa using h .univ + +theorem IsClub.isStationary [Nonempty α] [WellFoundedLT α] (hα : cof α ≠ ℵ₀) (hs : IsClub s) : + IsStationary s := + fun _ ht ↦ (hs.inter hα ht).nonempty + +/-- Non-stationary sets form an ideal. -/ +theorem not_isStationary_union [WellFoundedLT α] (hα : cof α ≠ ℵ₀) + (hs : ¬ IsStationary s) (ht : ¬ IsStationary t) : ¬ IsStationary (s ∪ t) := by + simp_rw [IsStationary, not_forall, Set.not_nonempty_iff_eq_empty] at hs ht ⊢ + obtain ⟨u, hu, hsu⟩ := hs + obtain ⟨v, hv, htv⟩ := ht + refine ⟨_, hu.inter hα hv, ?_⟩ + grind + +theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal (sᶜ)) : IsStationary s := by + intro t ht + obtain ⟨a, ha⟩ := not_isCofinal_iff.1 hs + obtain ⟨b, hb, hb'⟩ := ht.isCofinal a + refine ⟨b, ?_, hb⟩ + contrapose! ha + exact ⟨b, ha, hb'⟩ + +theorem isStationary_iff_not_isCofinal_compl [WellFoundedLT α] (hα : cof α ≤ ℵ₀) : + IsStationary s ↔ ¬ IsCofinal (sᶜ) where + mp hs h := by + obtain ⟨t, hts, ht, htα⟩ := ord_cof_eq_of_isCofinal h + have ht' := dirSupClosed_of_type_le_omega0 ht (htα.trans_le ?_) + · cases hs ⟨ht', ht⟩ + grind + · simpa using ord_mono hα + mpr := .of_not_isCofinal_compl From 87bba65094778fb7829004ee2a8ad9699f57ba94 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 22 May 2026 17:04:49 -0600 Subject: [PATCH 13/24] more --- Mathlib/SetTheory/Cardinal/Cofinality/Club.lean | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index e2efa682bbd307..47f388e40aa2e0 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -5,7 +5,9 @@ Authors: Violeta Hernández Palacios -/ module -public import Mathlib.SetTheory.Cardinal.Cofinality.Ordinal +public import Mathlib.Order.DirSupClosed +public import Mathlib.Order.IsNormal +public import Mathlib.SetTheory.Cardinal.Cofinality.Basic /-! # Club sets @@ -196,13 +198,3 @@ theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal (sᶜ)) : IsStati refine ⟨b, ?_, hb⟩ contrapose! ha exact ⟨b, ha, hb'⟩ - -theorem isStationary_iff_not_isCofinal_compl [WellFoundedLT α] (hα : cof α ≤ ℵ₀) : - IsStationary s ↔ ¬ IsCofinal (sᶜ) where - mp hs h := by - obtain ⟨t, hts, ht, htα⟩ := ord_cof_eq_of_isCofinal h - have ht' := dirSupClosed_of_type_le_omega0 ht (htα.trans_le ?_) - · cases hs ⟨ht', ht⟩ - grind - · simpa using ord_mono hα - mpr := .of_not_isCofinal_compl From 9acee7fc5b99e59e4d556893dc45bcb25fc284c5 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 22 May 2026 17:05:57 -0600 Subject: [PATCH 14/24] finish --- Mathlib/Order/Cofinal.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Mathlib/Order/Cofinal.lean b/Mathlib/Order/Cofinal.lean index 0e8b480d90627f..c3376807934a07 100644 --- a/Mathlib/Order/Cofinal.lean +++ b/Mathlib/Order/Cofinal.lean @@ -53,6 +53,11 @@ theorem IsCofinal.mono {s t : Set α} (h : s ⊆ t) (hs : IsCofinal s) : IsCofin obtain ⟨b, hb, hb'⟩ := hs a exact ⟨b, h hb, hb'⟩ +theorem IsCofinal.nonempty [Nonempty α] {s : Set α} (h : IsCofinal s) : s.Nonempty := by + inhabit α + obtain ⟨x, hx, _⟩ := h default + exact ⟨x, hx⟩ + end LE section Preorder From 3b0502624208438bb33eb9545091532c00ccc29a Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 22 May 2026 17:08:13 -0600 Subject: [PATCH 15/24] not using yet --- Mathlib/SetTheory/Cardinal/Cofinality/Club.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index 47f388e40aa2e0..7f0853c8a6de9c 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -12,9 +12,11 @@ public import Mathlib.SetTheory.Cardinal.Cofinality.Basic /-! # Club sets -A subset of a well-ordered type `α` is called a club set when it is closed in the order topology and -cofinal. If `α` has no maximum, then an equivalent condition is that `α` is closed and unbounded; -hence the name. +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 **stationary set** is a set which intersects all club sets. ## Implementation notes @@ -27,7 +29,7 @@ public section universe u v -open Cardinal Order Ordinal +open Cardinal Order /-- A club set is closed under suprema and cofinal. -/ structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where From e65606777d5e5db4559d1afab424a33056c2d235 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 22 May 2026 17:13:55 -0600 Subject: [PATCH 16/24] revert --- Mathlib/SetTheory/Cardinal/Cofinality/Club.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index 7f0853c8a6de9c..e79f563803963e 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -129,7 +129,7 @@ theorem IsClub.inter {s t : Set α} (hα : cof α ≠ ℵ₀) (hs : IsClub s) (h rw [← Set.sInter_pair] have H : ∀ x ∈ ({s, t} : Set _), IsClub x := by simpa [hs] obtain hα | hα' := hα.lt_or_gt - · rw [Order.cof_lt_aleph0_iff] at hα + · rw [cof_lt_aleph0_iff] at hα exact .sInter_of_cof_le_one hα H · exact .sInter hα (hα'.trans_le' <| by simp) H From 122721a4f654f3cfdfa4c528ef81c39ef2e13b7d Mon Sep 17 00:00:00 2001 From: vihdzp Date: Fri, 22 May 2026 18:34:43 -0600 Subject: [PATCH 17/24] more theorems --- .../SetTheory/Cardinal/Cofinality/Club.lean | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index e79f563803963e..80da32bb7c0097 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -184,7 +184,24 @@ theorem IsClub.isStationary [Nonempty α] [WellFoundedLT α] (hα : cof α ≠ IsStationary s := fun _ ht ↦ (hs.inter hα ht).nonempty -/-- Non-stationary sets form an ideal. -/ +theorem not_isStationary_sUnion [WellFoundedLT α] {s : Set (Set α)} (hα : cof α ≠ ℵ₀) + (hsα : #s < cof α) (hs : ∀ x ∈ s, ¬ IsStationary x) : ¬ IsStationary (⋃₀ s) := by + simp_rw [IsStationary, not_forall, Set.not_nonempty_iff_eq_empty, + ← Set.disjoint_iff_inter_eq_empty] at hs ⊢ + choose f hf hf' using hs + refine ⟨⋂ x : s, f _ x.2, ?_, ?_⟩ + · apply IsClub.iInter hα <;> simpa + · rw [Set.disjoint_sUnion_left] + exact fun x hx ↦ (hf' _ hx).mono_right <| Set.iInter_subset (fun x : s ↦ f x.1 x.2) ⟨x, hx⟩ + +theorem not_isStationary_iUnion [WellFoundedLT α] {ι : Type u} {f : ι → Set α} (hα : cof α ≠ ℵ₀) + (hι : Cardinal.lift.{v} #ι < Cardinal.lift.{u} (cof α)) (hf : ∀ i, ¬ IsStationary (f i)) : + ¬ IsStationary (⋃ i, f i) := by + rw [← Set.sUnion_range] + refine not_isStationary_sUnion hα ?_ (by simpa) + rw [← Cardinal.lift_lt] + exact mk_range_le_lift.trans_lt hι + theorem not_isStationary_union [WellFoundedLT α] (hα : cof α ≠ ℵ₀) (hs : ¬ IsStationary s) (ht : ¬ IsStationary t) : ¬ IsStationary (s ∪ t) := by simp_rw [IsStationary, not_forall, Set.not_nonempty_iff_eq_empty] at hs ht ⊢ From 8de73c077cd23727f2b974d3c224577adc9fab80 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sat, 23 May 2026 04:11:22 -0600 Subject: [PATCH 18/24] spacing --- Mathlib/SetTheory/Cardinal/Cofinality/Club.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index 80da32bb7c0097..db6c52e9379076 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -210,7 +210,7 @@ theorem not_isStationary_union [WellFoundedLT α] (hα : cof α ≠ ℵ₀) refine ⟨_, hu.inter hα hv, ?_⟩ grind -theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal (sᶜ)) : IsStationary s := by +theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal sᶜ) : IsStationary s := by intro t ht obtain ⟨a, ha⟩ := not_isCofinal_iff.1 hs obtain ⟨b, hb, hb'⟩ := ht.isCofinal a From 5b7dd80eb1c757c1a8f38d6a09abdf3c3006cb31 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sat, 23 May 2026 04:46:16 -0600 Subject: [PATCH 19/24] generalize --- .../SetTheory/Cardinal/Cofinality/Club.lean | 99 ++++++++++--------- 1 file changed, 53 insertions(+), 46 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index db6c52e9379076..cae16cb792cac6 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -29,7 +29,7 @@ public section universe u v -open Cardinal Order +open Cardinal Order Set /-- A club set is closed under suprema and cofinal. -/ structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where @@ -57,7 +57,7 @@ theorem isClub_empty_iff : IsClub (α := α) ∅ ↔ IsEmpty α := ⟨fun h ↦ isCofinal_empty_iff.1 h.isCofinal, fun _ ↦ .of_isEmpty⟩ theorem IsClub.union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) := - ⟨hs.dirSupClosed.union ht.dirSupClosed, hs.isCofinal.mono Set.subset_union_left⟩ + ⟨hs.dirSupClosed.union ht.dirSupClosed, hs.isCofinal.mono subset_union_left⟩ theorem IsClub.isLUB_mem (hs : IsClub s) (ht : t ⊆ s) (ht₀ : t.Nonempty) (hx : IsLUB t x) : x ∈ s := hs.dirSupClosed ht ht₀ (.of_linearOrder _) hx @@ -69,12 +69,12 @@ theorem IsClub.csSup_mem {α} [ConditionallyCompleteLinearOrder α] {s t : Set theorem IsClub.sInter_of_orderTop {s : Set (Set α)} [OrderTop α] (hs : ∀ x ∈ s, IsClub x) : IsClub (⋂₀ s) := by refine ⟨.sInter fun x hx ↦ (hs x hx).dirSupClosed, ?_⟩ - rw [isCofinal_iff_top_mem, Set.mem_sInter] + rw [isCofinal_iff_top_mem, mem_sInter] exact fun x hx ↦ (hs x hx).isCofinal.top_mem theorem IsClub.iInter_of_orderTop {ι : Type*} {f : ι → Set α} [OrderTop α] (hs : ∀ i, IsClub (f i)) : IsClub (⋂ i, f i) := by - rw [← Set.sInter_range] + rw [← sInter_range] exact .sInter_of_orderTop (by simpa) theorem IsClub.sInter_of_cof_le_one {s : Set (Set α)} (hα : cof α ≤ 1) @@ -86,11 +86,10 @@ theorem IsClub.sInter_of_cof_le_one {s : Set (Set α)} (hα : cof α ≤ 1) theorem IsClub.iInter_of_cof_le_one {ι : Type*} {f : ι → Set α} (hα : cof α ≤ 1) (hs : ∀ i, IsClub (f i)) : IsClub (⋂ i, f i) := by - rw [← Set.sInter_range] + rw [← sInter_range] exact .sInter_of_cof_le_one hα (by simpa) section WellFoundedLT - variable [WellFoundedLT α] attribute [local instance] @@ -108,7 +107,7 @@ theorem IsClub.sInter {s : Set (Set α)} (hα : cof α ≠ ℵ₀) (hsα : #s < refine .of_not_isCofinal fun hg ↦ (cof_le hg).not_gt (hα.trans_le' ?_) simpa using mk_range_le_lift (f := g) refine ⟨_, fun t ht ↦ ?_, le_csSup hg ⟨0, rfl⟩⟩ - apply (hs t ht).isLUB_mem (t := .range fun n ↦ f ⟨t, ht⟩ (g n)) _ (Set.range_nonempty _) + apply (hs t ht).isLUB_mem (t := .range fun n ↦ f ⟨t, ht⟩ (g n)) _ (range_nonempty _) · refine ⟨?_, fun b hb ↦ csSup_le' ?_⟩ <;> rintro _ ⟨n, rfl⟩ · apply (le_csSup (.of_not_isCofinal _) _).trans (le_csSup hg ⟨n + 1, rfl⟩) · exact fun hg' ↦ (cof_le hg').not_gt (mk_range_le.trans_lt hsα) @@ -117,16 +116,14 @@ theorem IsClub.sInter {s : Set (Set α)} (hα : cof α ≠ ℵ₀) (hsα : #s < · grind theorem IsClub.iInter {ι : Type u} {f : ι → Set α} (hα : cof α ≠ ℵ₀) - (hι : Cardinal.lift.{v} #ι < Cardinal.lift.{u} (cof α)) (hf : ∀ i, IsClub (f i)) : - IsClub (⋂ i, f i) := by - rw [← Set.sInter_range] + (hι : lift.{v} #ι < lift.{u} (cof α)) (hf : ∀ i, IsClub (f i)) : IsClub (⋂ i, f i) := by + rw [← sInter_range] refine IsClub.sInter hα ?_ (by simpa) rw [← Cardinal.lift_lt] exact mk_range_le_lift.trans_lt hι -theorem IsClub.inter {s t : Set α} (hα : cof α ≠ ℵ₀) (hs : IsClub s) (ht : IsClub t) : - IsClub (s ∩ t) := by - rw [← Set.sInter_pair] +theorem IsClub.inter (hα : cof α ≠ ℵ₀) (hs : IsClub s) (ht : IsClub t) : IsClub (s ∩ t) := by + rw [← sInter_pair] have H : ∀ x ∈ ({s, t} : Set _), IsClub x := by simpa [hs] obtain hα | hα' := hα.lt_or_gt · rw [cof_lt_aleph0_iff] at hα @@ -140,7 +137,7 @@ theorem Order.IsNormal.isClub_fixedPoints {f : α → α} (hα : cof α ≠ ℵ 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'] + · rwa [image_congr hs, image_id'] · cases topOrderOrNoTopOrder α with | inl => use ⊤; simpa using hf.strictMono.id_le ⊤ | inr h => @@ -160,15 +157,18 @@ end WellFoundedLT def IsStationary (s : Set α) : Prop := ∀ ⦃t⦄, IsClub t → (s ∩ t).Nonempty +theorem not_isStationary_iff : ¬ IsStationary s ↔ ∃ t, IsClub t ∧ Disjoint s t := by + simp [IsStationary, disjoint_iff, not_nonempty_iff_eq_empty] + @[gcongr] theorem IsStationary.mono (hs : IsStationary s) (h : s ⊆ t) : IsStationary t := - fun _u hu ↦ (hs hu).mono (Set.inter_subset_inter_left _ h) + fun _u hu ↦ (hs hu).mono (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 [IsStationary, ← not_imp_not (b := IsClub _), Set.not_nonempty_iff_eq_empty, + simp [IsStationary, ← not_imp_not (b := IsClub _), not_nonempty_iff_eq_empty, isClub_empty_iff] @[simp] @@ -180,36 +180,6 @@ theorem not_isStationary_empty : ¬ IsStationary (∅ : Set α) := by intro h simpa using h .univ -theorem IsClub.isStationary [Nonempty α] [WellFoundedLT α] (hα : cof α ≠ ℵ₀) (hs : IsClub s) : - IsStationary s := - fun _ ht ↦ (hs.inter hα ht).nonempty - -theorem not_isStationary_sUnion [WellFoundedLT α] {s : Set (Set α)} (hα : cof α ≠ ℵ₀) - (hsα : #s < cof α) (hs : ∀ x ∈ s, ¬ IsStationary x) : ¬ IsStationary (⋃₀ s) := by - simp_rw [IsStationary, not_forall, Set.not_nonempty_iff_eq_empty, - ← Set.disjoint_iff_inter_eq_empty] at hs ⊢ - choose f hf hf' using hs - refine ⟨⋂ x : s, f _ x.2, ?_, ?_⟩ - · apply IsClub.iInter hα <;> simpa - · rw [Set.disjoint_sUnion_left] - exact fun x hx ↦ (hf' _ hx).mono_right <| Set.iInter_subset (fun x : s ↦ f x.1 x.2) ⟨x, hx⟩ - -theorem not_isStationary_iUnion [WellFoundedLT α] {ι : Type u} {f : ι → Set α} (hα : cof α ≠ ℵ₀) - (hι : Cardinal.lift.{v} #ι < Cardinal.lift.{u} (cof α)) (hf : ∀ i, ¬ IsStationary (f i)) : - ¬ IsStationary (⋃ i, f i) := by - rw [← Set.sUnion_range] - refine not_isStationary_sUnion hα ?_ (by simpa) - rw [← Cardinal.lift_lt] - exact mk_range_le_lift.trans_lt hι - -theorem not_isStationary_union [WellFoundedLT α] (hα : cof α ≠ ℵ₀) - (hs : ¬ IsStationary s) (ht : ¬ IsStationary t) : ¬ IsStationary (s ∪ t) := by - simp_rw [IsStationary, not_forall, Set.not_nonempty_iff_eq_empty] at hs ht ⊢ - obtain ⟨u, hu, hsu⟩ := hs - obtain ⟨v, hv, htv⟩ := ht - refine ⟨_, hu.inter hα hv, ?_⟩ - grind - theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal sᶜ) : IsStationary s := by intro t ht obtain ⟨a, ha⟩ := not_isCofinal_iff.1 hs @@ -217,3 +187,40 @@ theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal sᶜ) : IsStation refine ⟨b, ?_, hb⟩ contrapose! ha exact ⟨b, ha, hb'⟩ + +section WellFoundedLT +variable [WellFoundedLT α] + +theorem IsClub.isStationary [Nonempty α] (hα : cof α ≠ ℵ₀) (hs : IsClub s) : IsStationary s := + fun _ ht ↦ (hs.inter hα ht).nonempty + +theorem isStationary_sUnion_iff {s : Set (Set α)} (hα : cof α ≠ ℵ₀) (hsα : #s < cof α) : + IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x where + mp h := by + contrapose! h + simp_rw [not_isStationary_iff] at h ⊢ + choose f hf hxf using h + refine ⟨⋂ x : s, f _ x.2, ?_, ?_⟩ + · apply IsClub.iInter hα <;> simpa + · rw [disjoint_sUnion_left] + exact fun x hx ↦ (hxf _ hx).mono_right (iInter_subset _ ⟨x, hx⟩) + mpr := fun ⟨x, hxs, hx⟩ ↦ hx.mono (subset_sUnion_of_mem hxs) + +theorem isStationary_iUnion_iff {ι : Type u} {f : ι → Set α} (hα : cof α ≠ ℵ₀) + (hι : lift.{v} #ι < lift.{u} (cof α)) : IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i) := by + rw [← sUnion_range, isStationary_sUnion_iff hα] + · simp + · rw [← Cardinal.lift_lt] + exact mk_range_le_lift.trans_lt hι + +theorem isStationary_union_iff (hα : cof α ≠ ℵ₀) : + IsStationary (s ∪ t) ↔ IsStationary s ∨ IsStationary t where + mp h := by + contrapose! h + simp_rw [not_isStationary_iff, disjoint_iff_inter_eq_empty] at h ⊢ + obtain ⟨⟨u, hu, hsu⟩, ⟨v, hv, hsv⟩⟩ := h + refine ⟨_, hu.inter hα hv, ?_⟩ + grind + mpr h := h.elim (.mono · subset_union_left) (.mono · subset_union_right) + +end WellFoundedLT From 33bf92127674b9c40035497dcb6438a2faafcde6 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sat, 23 May 2026 05:07:10 -0600 Subject: [PATCH 20/24] evenmore --- .../SetTheory/Cardinal/Cofinality/Club.lean | 70 +++++++++++++++---- 1 file changed, 56 insertions(+), 14 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index cae16cb792cac6..615c9e0b74f7c7 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -122,13 +122,22 @@ theorem IsClub.iInter {ι : Type u} {f : ι → Set α} (hα : cof α ≠ ℵ₀ rw [← Cardinal.lift_lt] exact mk_range_le_lift.trans_lt hι +theorem IsClub.sInter_countable {s : Set (Set α)} (hα : cof α ≠ ℵ₀) (hsα : s.Countable) + (hs : ∀ x ∈ s, IsClub x) : IsClub (⋂₀ s) := by + obtain hα | hα := hα.lt_or_gt + · apply IsClub.sInter_of_cof_le_one _ hs + rwa [← cof_lt_aleph0_iff] + · apply IsClub.sInter hα.ne' (hα.trans_le' _) hs + rwa [le_aleph0_iff_set_countable] + +theorem IsClub.iInter_countable {ι : Type*} {f : ι → Set α} [Countable ι] (hα : cof α ≠ ℵ₀) + (hf : ∀ i, IsClub (f i)) : IsClub (⋂ i, f i) := by + rw [← sInter_range] + apply IsClub.sInter_countable hα (countable_range f) + simpa + theorem IsClub.inter (hα : cof α ≠ ℵ₀) (hs : IsClub s) (ht : IsClub t) : IsClub (s ∩ t) := by - rw [← sInter_pair] - have H : ∀ x ∈ ({s, t} : Set _), IsClub x := by simpa [hs] - obtain hα | hα' := hα.lt_or_gt - · rw [cof_lt_aleph0_iff] at hα - exact .sInter_of_cof_le_one hα H - · exact .sInter hα (hα'.trans_le' <| by simp) H + simpa [hs, ht] using IsClub.sInter_countable (s := {s, t}) hα theorem Order.IsNormal.isClub_range {f : α → α} (hf : IsNormal f) : IsClub (.range f) := ⟨hf.dirSupClosed_range, fun x ↦ ⟨_, ⟨x, rfl⟩, hf.strictMono.le_apply⟩⟩ @@ -188,6 +197,32 @@ theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal sᶜ) : IsStation contrapose! ha exact ⟨b, ha, hb'⟩ +theorem isStationary_sUnion_iff_of_cof_le_one {s : Set (Set α)} (hα : cof α ≤ 1) : + IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x where + mp h := by + contrapose! h + simp_rw [not_isStationary_iff] at h ⊢ + choose f hf hxf using h + refine ⟨⋂ x : s, f _ x.2, ?_, ?_⟩ + · apply IsClub.iInter_of_cof_le_one hα + simpa + · rw [disjoint_sUnion_left] + exact fun x hx ↦ (hxf _ hx).mono_right (iInter_subset _ ⟨x, hx⟩) + mpr := fun ⟨x, hxs, hx⟩ ↦ hx.mono (subset_sUnion_of_mem hxs) + +theorem isStationary_iUnion_iff_of_cof_le_one {ι : Type u} {f : ι → Set α} (hα : cof α ≤ 1) : + IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i) := by + rw [← sUnion_range, isStationary_sUnion_iff_of_cof_le_one hα] + simp + +theorem isStationary_sUnion_iff_of_orderTop [OrderTop α] {s : Set (Set α)} : + IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x := + isStationary_sUnion_iff_of_cof_le_one (by simp) + +theorem isStationary_iUnion_iff_of_orderTop [OrderTop α] {ι : Type u} {f : ι → Set α} : + IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i) := + isStationary_iUnion_iff_of_cof_le_one (by simp) + section WellFoundedLT variable [WellFoundedLT α] @@ -213,14 +248,21 @@ theorem isStationary_iUnion_iff {ι : Type u} {f : ι → Set α} (hα : cof α · rw [← Cardinal.lift_lt] exact mk_range_le_lift.trans_lt hι +theorem isStationary_sUnion_countable_iff {s : Set (Set α)} (hα : cof α ≠ ℵ₀) (hsα : s.Countable) : + IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x := by + obtain hα | hα := hα.lt_or_gt + · apply isStationary_sUnion_iff_of_cof_le_one + rwa [← cof_lt_aleph0_iff] + · apply isStationary_sUnion_iff hα.ne' (hα.trans_le' _) + rwa [le_aleph0_iff_set_countable] + +theorem isStationary_iUnion_countable_iff {ι : Type*} {f : ι → Set α} [Countable ι] + (hα : cof α ≠ ℵ₀) : IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i) := by + rw [← sUnion_range, isStationary_sUnion_countable_iff hα (countable_range f)] + simp + theorem isStationary_union_iff (hα : cof α ≠ ℵ₀) : - IsStationary (s ∪ t) ↔ IsStationary s ∨ IsStationary t where - mp h := by - contrapose! h - simp_rw [not_isStationary_iff, disjoint_iff_inter_eq_empty] at h ⊢ - obtain ⟨⟨u, hu, hsu⟩, ⟨v, hv, hsv⟩⟩ := h - refine ⟨_, hu.inter hα hv, ?_⟩ - grind - mpr h := h.elim (.mono · subset_union_left) (.mono · subset_union_right) + IsStationary (s ∪ t) ↔ IsStationary s ∨ IsStationary t := by + simpa using isStationary_sUnion_countable_iff (s := {s, t}) hα end WellFoundedLT From 1d05495effc75175fce73cdd6b7971f2afb591b2 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sat, 23 May 2026 11:01:15 -0600 Subject: [PATCH 21/24] suggestion --- Mathlib/SetTheory/Cardinal/Cofinality/Club.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index 615c9e0b74f7c7..4d1e4f8ffde824 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -248,21 +248,21 @@ theorem isStationary_iUnion_iff {ι : Type u} {f : ι → Set α} (hα : cof α · rw [← Cardinal.lift_lt] exact mk_range_le_lift.trans_lt hι -theorem isStationary_sUnion_countable_iff {s : Set (Set α)} (hα : cof α ≠ ℵ₀) (hsα : s.Countable) : - IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x := by +theorem isStationary_sUnion_iff_of_countable {s : Set (Set α)} (hα : cof α ≠ ℵ₀) + (hsα : s.Countable) : IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x := by obtain hα | hα := hα.lt_or_gt · apply isStationary_sUnion_iff_of_cof_le_one rwa [← cof_lt_aleph0_iff] · apply isStationary_sUnion_iff hα.ne' (hα.trans_le' _) rwa [le_aleph0_iff_set_countable] -theorem isStationary_iUnion_countable_iff {ι : Type*} {f : ι → Set α} [Countable ι] +theorem isStationary_iUnion_iff_of_countable {ι : Type*} {f : ι → Set α} [Countable ι] (hα : cof α ≠ ℵ₀) : IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i) := by - rw [← sUnion_range, isStationary_sUnion_countable_iff hα (countable_range f)] + rw [← sUnion_range, isStationary_sUnion_iff_of_countable hα (countable_range f)] simp theorem isStationary_union_iff (hα : cof α ≠ ℵ₀) : IsStationary (s ∪ t) ↔ IsStationary s ∨ IsStationary t := by - simpa using isStationary_sUnion_countable_iff (s := {s, t}) hα + simpa using isStationary_sUnion_iff_of_countable (s := {s, t}) hα end WellFoundedLT From e7cb9beabc449709a28cc581f7c7fa06e9a1ccca Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sat, 23 May 2026 22:14:17 -0600 Subject: [PATCH 22/24] suggestions --- Mathlib/Order/Interval/Set/Basic.lean | 2 +- Mathlib/SetTheory/Cardinal/Cofinality/Club.lean | 6 +++++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/Mathlib/Order/Interval/Set/Basic.lean b/Mathlib/Order/Interval/Set/Basic.lean index 98c6874023d414..46ee9677bc7590 100644 --- a/Mathlib/Order/Interval/Set/Basic.lean +++ b/Mathlib/Order/Interval/Set/Basic.lean @@ -468,7 +468,7 @@ variable [PartialOrder α] {a b c : α} @[simp] theorem Icc_self (a : α) : Icc a a = {a} := - Set.ext <| by simp [Icc, le_antisymm_iff, and_comm] + ext <| by simp [Icc, le_antisymm_iff, and_comm] instance instIccUnique : Unique (Icc a a) where default := ⟨a, by simp⟩ diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index 4d1e4f8ffde824..3277cf7ee435e3 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -181,7 +181,7 @@ theorem isStationary_univ_iff : IsStationary (.univ (α := α)) ↔ Nonempty α isClub_empty_iff] @[simp] -theorem IsStationary.univ [Nonempty α] : IsStationary (.univ (α := α)) := +protected theorem IsStationary.univ [Nonempty α] : IsStationary (.univ (α := α)) := isStationary_univ_iff.2 ‹_› @[simp] @@ -189,6 +189,10 @@ theorem not_isStationary_empty : ¬ IsStationary (∅ : Set α) := by intro h simpa using h .univ +@[simp] +theorem not_isStationary_of_isEmpty [IsEmpty α] : ¬ IsStationary s := + s.eq_empty_of_isEmpty ▸ not_isStationary_empty + theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal sᶜ) : IsStationary s := by intro t ht obtain ⟨a, ha⟩ := not_isCofinal_iff.1 hs From 0746b296573530eec00be82684c0f206a5eef488 Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 24 May 2026 07:42:10 -0600 Subject: [PATCH 23/24] suggestion --- Mathlib/SetTheory/Cardinal/Cofinality/Club.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean index 3277cf7ee435e3..e2426c09d236f5 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -122,7 +122,7 @@ theorem IsClub.iInter {ι : Type u} {f : ι → Set α} (hα : cof α ≠ ℵ₀ rw [← Cardinal.lift_lt] exact mk_range_le_lift.trans_lt hι -theorem IsClub.sInter_countable {s : Set (Set α)} (hα : cof α ≠ ℵ₀) (hsα : s.Countable) +theorem IsClub.sInter_of_countable {s : Set (Set α)} (hα : cof α ≠ ℵ₀) (hsα : s.Countable) (hs : ∀ x ∈ s, IsClub x) : IsClub (⋂₀ s) := by obtain hα | hα := hα.lt_or_gt · apply IsClub.sInter_of_cof_le_one _ hs @@ -130,14 +130,14 @@ theorem IsClub.sInter_countable {s : Set (Set α)} (hα : cof α ≠ ℵ₀) (hs · apply IsClub.sInter hα.ne' (hα.trans_le' _) hs rwa [le_aleph0_iff_set_countable] -theorem IsClub.iInter_countable {ι : Type*} {f : ι → Set α} [Countable ι] (hα : cof α ≠ ℵ₀) +theorem IsClub.iInter_of_countable {ι : Type*} {f : ι → Set α} [Countable ι] (hα : cof α ≠ ℵ₀) (hf : ∀ i, IsClub (f i)) : IsClub (⋂ i, f i) := by rw [← sInter_range] - apply IsClub.sInter_countable hα (countable_range f) + apply IsClub.sInter_of_countable hα (countable_range f) simpa theorem IsClub.inter (hα : cof α ≠ ℵ₀) (hs : IsClub s) (ht : IsClub t) : IsClub (s ∩ t) := by - simpa [hs, ht] using IsClub.sInter_countable (s := {s, t}) hα + simpa [hs, ht] using IsClub.sInter_of_countable (s := {s, t}) hα theorem Order.IsNormal.isClub_range {f : α → α} (hf : IsNormal f) : IsClub (.range f) := ⟨hf.dirSupClosed_range, fun x ↦ ⟨_, ⟨x, rfl⟩, hf.strictMono.le_apply⟩⟩ From a7301dcc03f8359ccd9197fc60ed12ee1311293b Mon Sep 17 00:00:00 2001 From: vihdzp Date: Sun, 24 May 2026 09:10:46 -0600 Subject: [PATCH 24/24] why is this here --- Mathlib/Order/Interval/Set/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Order/Interval/Set/Basic.lean b/Mathlib/Order/Interval/Set/Basic.lean index 0c4ffd2e45c6cb..fb6b4ec90b2c7c 100644 --- a/Mathlib/Order/Interval/Set/Basic.lean +++ b/Mathlib/Order/Interval/Set/Basic.lean @@ -472,7 +472,7 @@ variable [PartialOrder α] {a b c : α} @[simp] theorem Icc_self (a : α) : Icc a a = {a} := - ext <| by simp [Icc, le_antisymm_iff, and_comm] + Set.ext <| by simp [Icc, le_antisymm_iff, and_comm] instance instIccUnique : Unique (Icc a a) where default := ⟨a, by simp⟩