diff --git a/Mathlib.lean b/Mathlib.lean index 49a4130a24ce7c..ff97686161654c 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5981,7 +5981,8 @@ public import Mathlib.Order.Defs.LinearOrder public import Mathlib.Order.Defs.PartialOrder public import Mathlib.Order.Defs.Prop 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/Data/Fintype/Order.lean b/Mathlib/Data/Fintype/Order.lean index 616051ccc6ca7f..df1b5dcaf8d39c 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/Cofinal.lean b/Mathlib/Order/Cofinal.lean index ce94954545c4d6..0eddfbd7bccbca 100644 --- a/Mathlib/Order/Cofinal.lean +++ b/Mathlib/Order/Cofinal.lean @@ -52,6 +52,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 diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed/Basic.lean similarity index 97% rename from Mathlib/Order/DirSupClosed.lean rename to Mathlib/Order/DirSupClosed/Basic.lean index ead09bf1ac225a..9816253c8526c3 100644 --- a/Mathlib/Order/DirSupClosed.lean +++ b/Mathlib/Order/DirSupClosed/Basic.lean @@ -288,17 +288,21 @@ lemma dirSupInaccOn_Iic (a : α) : DirSupInaccOn D (Iic a) := end Preorder -namespace PartialOrder +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 end PartialOrder diff --git a/Mathlib/Order/DirSupClosed/Finite.lean b/Mathlib/Order/DirSupClosed/Finite.lean new file mode 100644 index 00000000000000..84a2fb4650b209 --- /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 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⟩ diff --git a/Mathlib/Order/IsNormal.lean b/Mathlib/Order/IsNormal.lean index 12bcea021d6a7a..4b41bdb9883596 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 f772f2c6ae1fb6..e07364e5b93dbb 100644 --- a/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean +++ b/Mathlib/SetTheory/Cardinal/Cofinality/Club.lean @@ -5,16 +5,18 @@ 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 /-! # 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,9 @@ public section universe u v -open Cardinal Order +open Cardinal Order Set + +variable {α : Type v} {s t : Set α} {x : α} [LinearOrder α] /-- A club set is closed under suprema and cofinal. -/ structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where @@ -40,8 +44,6 @@ structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where namespace IsClub -variable {α : Type v} {s t : Set α} {x : α} [LinearOrder α] - @[simp] theorem of_isEmpty [IsEmpty α] {s : Set α} : IsClub s := ⟨.of_isEmpty, .of_isEmpty⟩ @@ -50,6 +52,12 @@ theorem of_isEmpty [IsEmpty α] {s : Set α} : IsClub s := protected theorem univ : IsClub (α := α) .univ := ⟨.univ, .univ⟩ +protected theorem 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⟩ + protected theorem union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) := ⟨hs.dirSupClosed.union ht.dirSupClosed, hs.isCofinal.mono Set.subset_union_left⟩ @@ -63,12 +71,12 @@ theorem csSup_mem {α} [ConditionallyCompleteLinearOrder α] {s t : Set α} theorem 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 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 sInter_of_cof_le_one {s : Set (Set α)} (hα : cof α ≤ 1) (hs : ∀ x ∈ s, IsClub x) : @@ -80,11 +88,10 @@ theorem sInter_of_cof_le_one {s : Set (Set α)} (hα : cof α ≤ 1) (hs : ∀ x theorem 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] @@ -102,7 +109,7 @@ protected theorem 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α) @@ -113,19 +120,27 @@ protected theorem sInter {s : Set (Set α)} (hα : cof α ≠ ℵ₀) (hsα : #s protected theorem 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] + rw [← sInter_range] refine IsClub.sInter hα ?_ (by simpa) rw [← Cardinal.lift_lt] exact mk_range_le_lift.trans_lt hι -protected theorem inter {s t : Set α} (hα : cof α ≠ ℵ₀) (hs : IsClub s) (ht : IsClub t) : - IsClub (s ∩ t) := by - rw [← Set.sInter_pair] - have H : ∀ x ∈ ({s, t} : Set _), IsClub x := by simpa [hs] - obtain hα | hα' := hα.lt_or_gt - · rw [cof_lt_aleph0_iff] at hα - exact .sInter_of_cof_le_one hα H - · exact .sInter hα (hα'.trans_le' <| by simp) H +theorem 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 + rwa [← cof_lt_aleph0_iff] + · apply IsClub.sInter hα.ne' (hα.trans_le' _) hs + rwa [le_aleph0_iff_set_countable] + +theorem 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_of_countable hα (countable_range f) + simpa + +protected theorem inter (hα : cof α ≠ ℵ₀) (hs : IsClub s) (ht : IsClub t) : IsClub (s ∩ t) := by + simpa [hs, ht] using IsClub.sInter_of_countable (s := {s, t}) hα theorem _root_.Order.IsNormal.isClub_range {f : α → α} (hf : IsNormal f) : IsClub (.range f) := ⟨hf.dirSupClosed_range, fun x ↦ ⟨_, ⟨x, rfl⟩, hf.strictMono.le_apply⟩⟩ @@ -134,7 +149,7 @@ theorem _root_.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 => @@ -147,3 +162,115 @@ theorem _root_.Order.IsNormal.isClub_fixedPoints {f : α → α} (hα : cof α end WellFoundedLT end IsClub + +/-! ### 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 + +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 (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 _), not_nonempty_iff_eq_empty, + isClub_empty_iff] + +@[simp] +protected theorem IsStationary.univ [Nonempty α] : IsStationary (.univ (α := α)) := + isStationary_univ_iff.2 ‹_› + +@[simp] +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 + obtain ⟨b, hb, hb'⟩ := ht.isCofinal a + refine ⟨b, ?_, hb⟩ + 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 α] + +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_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_iff_of_countable {ι : Type*} {f : ι → Set α} [Countable ι] + (hα : cof α ≠ ℵ₀) : IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i) := by + 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_iff_of_countable (s := {s, t}) hα + +end WellFoundedLT diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean index 2b981eef602627..4b490df2900437 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 @@ -180,8 +182,9 @@ theorem exists_ord_cof_eq_of_isCofinal [LinearOrder α] [WellFoundedLT α] · rw [← ht'] exact ((Subtype.strictMono_coe _).strictMonoOn _).orderIso.ordinalType_congr.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'⟩ := exists_ord_cof_eq α rw [← hs', cof_type, cof_eq_of_isCofinal hs] @@ -192,6 +195,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 + · 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 + rw [← hfs] at hs ⊢ + exact dirSupClosed_range_nat ((Subtype.mono_coe _).comp e.monotone) hs + /-! ### Cofinalities and suprema -/ section LinearOrder diff --git a/Mathlib/Topology/Order/ScottTopology.lean b/Mathlib/Topology/Order/ScottTopology.lean index 583db890a253ff..71659b8b46d925 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