Documentation

Mathlib.SetTheory.Cardinal.Cofinality.Club

Club sets and stationary sets #

A subset of a well-ordered type α is called a club set when it is closed in the order topology and cofinal. If α has no maximum, then an equivalent condition is that α is closed and unbounded; hence the name.

A stationary set is a set which intersects all club sets.

Implementation notes #

To avoid importing topology in the ordinals, we spell out the closure property using DirSupClosed. For any type equipped with the Scott-Hausdorff topology (which includes well-orders with the order topology), DirSupClosed s and IsClosed s are equivalent predicates.

structure IsClub {α : Type u_1} [LinearOrder α] (s : Set α) :

A club set is a set that is closed under suprema and that is cofinal.

dirSupClosed : DirSupClosed s
Club sets are closed under suprema. If α is a well-order with the order topology, this condition is equivalent to IsClosed s.
isCofinal : IsCofinal s
Club sets are cofinal. If α has no maximum, this condition is equivalent to ¬ BddAbove s. See not_bddAbove_iff_isCofinal.

Instances For

theorem isClub_iff {α : Type u_1} [LinearOrder α] (s : Set α) :

IsClub s ↔ DirSupClosed s ∧ IsCofinal s

@[simp]

theorem IsClub.of_isEmpty {α : Type v} [LinearOrder α] [IsEmpty α] {s : Set α} :

@[simp]

theorem IsClub.univ {α : Type v} [LinearOrder α] :

IsClub Set.univ

theorem IsClub.nonempty {α : Type v} {s : Set α} [LinearOrder α] [Nonempty α] (hs : IsClub s) :

theorem isClub_empty_iff {α : Type v} [LinearOrder α] :

IsClub ∅ ↔ IsEmpty α

theorem IsClub.union {α : Type v} {s t : Set α} [LinearOrder α] (hs : IsClub s) (ht : IsClub t) :

IsClub (s ∪ t)

theorem IsClub.isLUB_mem {α : Type v} {s t : Set α} {x : α} [LinearOrder α] (hs : IsClub s) (ht : t ⊆ s) (ht₀ : t.Nonempty) (hx : IsLUB t x) :

x ∈ s

theorem IsClub.csSup_mem {α : Type u_1} [ConditionallyCompleteLinearOrder α] {s t : Set α} (hs : IsClub s) (ht : t ⊆ s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) :

theorem IsClub.sInter_of_orderTop {α : Type v} [LinearOrder α] {s : Set (Set α)} [OrderTop α] (hs : ∀ x ∈ s, IsClub x) :

IsClub (⋂₀ s)

theorem IsClub.iInter_of_orderTop {α : Type v} [LinearOrder α] {ι : Type u_1} {f : ι → Set α} [OrderTop α] (hs : ∀ (i : ι), IsClub (f i)) :

IsClub (⋂ (i : ι), f i)

theorem IsClub.sInter_of_cof_le_one {α : Type v} [LinearOrder α] {s : Set (Set α)} (hα : Order.cof α ≤ 1) (hs : ∀ x ∈ s, IsClub x) :

IsClub (⋂₀ s)

theorem IsClub.iInter_of_cof_le_one {α : Type v} [LinearOrder α] {ι : Type u_1} {f : ι → Set α} (hα : Order.cof α ≤ 1) (hs : ∀ (i : ι), IsClub (f i)) :

IsClub (⋂ (i : ι), f i)

theorem IsClub.sInter {α : Type v} [LinearOrder α] [WellFoundedLT α] {s : Set (Set α)} (hα : Order.cof α ≠ Cardinal.aleph0) (hsα : Cardinal.mk ↑s < Order.cof α) (hs : ∀ x ∈ s, IsClub x) :

IsClub (⋂₀ s)

theorem IsClub.iInter {α : Type v} [LinearOrder α] [WellFoundedLT α] {ι : Type u} {f : ι → Set α} (hα : Order.cof α ≠ Cardinal.aleph0) (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < Cardinal.lift.{u, v} (Order.cof α)) (hf : ∀ (i : ι), IsClub (f i)) :

IsClub (⋂ (i : ι), f i)

theorem IsClub.sInter_of_countable {α : Type v} [LinearOrder α] [WellFoundedLT α] {s : Set (Set α)} (hα : Order.cof α ≠ Cardinal.aleph0) (hsα : s.Countable) (hs : ∀ x ∈ s, IsClub x) :

IsClub (⋂₀ s)

theorem IsClub.iInter_of_countable {α : Type v} [LinearOrder α] [WellFoundedLT α] {ι : Sort u_1} {f : ι → Set α} [Countable ι] (hα : Order.cof α ≠ Cardinal.aleph0) (hf : ∀ (i : ι), IsClub (f i)) :

IsClub (⋂ (i : ι), f i)

theorem IsClub.inter {α : Type v} {s t : Set α} [LinearOrder α] [WellFoundedLT α] (hα : Order.cof α ≠ Cardinal.aleph0) (hs : IsClub s) (ht : IsClub t) :

IsClub (s ∩ t)

theorem Order.IsNormal.isClub_range {α : Type v} [LinearOrder α] [WellFoundedLT α] {f : α → α} (hf : IsNormal f) :

IsClub (Set.range f)

theorem Order.IsNormal.isClub_fixedPoints {α : Type v} [LinearOrder α] [WellFoundedLT α] {f : α → α} (hα : cof α ≠ Cardinal.aleph0) (hf : IsNormal f) :

IsClub (Function.fixedPoints f)

theorem Order.isNormal_enum_iff_isClub {α : Type v} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] {s : Set α} {hs : IsCofinal s} :

IsNormal (Subtype.val ∘ ⇑(enum s hs)) ↔ IsClub s

Club sets in regular cardinals correspond one to one with normal functions.

theorem IsClub.isNormal_enum {α : Type v} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] {s : Set α} (hs : IsClub s) :

Order.IsNormal (Subtype.val ∘ ⇑(Order.enum s ⋯))

Stationary sets #

def IsStationary {α : Type v} [LinearOrder α] (s : Set α) :

A set is called stationary when it intersects all club sets.

Equations

IsStationary s = ∀ ⦃t : Set α⦄, IsClub t → (s ∩ t).Nonempty

Instances For

theorem not_isStationary_iff {α : Type v} {s : Set α} [LinearOrder α] :

¬IsStationary s ↔ ∃ (t : Set α), IsClub t ∧ Disjoint s t

theorem IsStationary.mono {α : Type v} {s t : Set α} [LinearOrder α] (hs : IsStationary s) (h : s ⊆ t) :

theorem IsStationary.nonempty {α : Type v} {s : Set α} [LinearOrder α] (hs : IsStationary s) :

theorem isStationary_univ_iff {α : Type v} [LinearOrder α] :

IsStationary Set.univ ↔ Nonempty α

@[simp]

theorem IsStationary.univ {α : Type v} [LinearOrder α] [Nonempty α] :

IsStationary Set.univ

@[simp]

theorem not_isStationary_empty {α : Type v} [LinearOrder α] :

¬IsStationary ∅

@[simp]

theorem not_isStationary_of_isEmpty {α : Type v} {s : Set α} [LinearOrder α] [IsEmpty α] :

¬IsStationary s

theorem IsStationary.of_not_isCofinal_compl {α : Type v} {s : Set α} [LinearOrder α] (hs : ¬IsCofinal sᶜ) :

theorem isStationary_sUnion_iff_of_cof_le_one {α : Type v} [LinearOrder α] {s : Set (Set α)} (hα : Order.cof α ≤ 1) :

IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x

theorem isStationary_iUnion_iff_of_cof_le_one {α : Type v} [LinearOrder α] {ι : Sort u_1} {f : ι → Set α} (hα : Order.cof α ≤ 1) :

IsStationary (⋃ (i : ι), f i) ↔ ∃ (i : ι), IsStationary (f i)

theorem isStationary_sUnion_iff_of_orderTop {α : Type v} [LinearOrder α] [OrderTop α] {s : Set (Set α)} :

IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x

theorem isStationary_iUnion_iff_of_orderTop {α : Type v} [LinearOrder α] [OrderTop α] {ι : Sort u_1} {f : ι → Set α} :

IsStationary (⋃ (i : ι), f i) ↔ ∃ (i : ι), IsStationary (f i)

theorem IsClub.isStationary {α : Type v} {s : Set α} [LinearOrder α] [WellFoundedLT α] [Nonempty α] (hα : Order.cof α ≠ Cardinal.aleph0) (hs : IsClub s) :

theorem isStationary_sUnion_iff {α : Type v} [LinearOrder α] [WellFoundedLT α] {s : Set (Set α)} (hα : Order.cof α ≠ Cardinal.aleph0) (hsα : Cardinal.mk ↑s < Order.cof α) :

IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x

theorem isStationary_iUnion_iff {α : Type v} [LinearOrder α] [WellFoundedLT α] {ι : Type u} {f : ι → Set α} (hα : Order.cof α ≠ Cardinal.aleph0) (hι : Cardinal.lift.{v, u} (Cardinal.mk ι) < Cardinal.lift.{u, v} (Order.cof α)) :

IsStationary (⋃ (i : ι), f i) ↔ ∃ (i : ι), IsStationary (f i)

theorem isStationary_sUnion_iff_of_countable {α : Type v} [LinearOrder α] [WellFoundedLT α] {s : Set (Set α)} (hα : Order.cof α ≠ Cardinal.aleph0) (hsα : s.Countable) :

IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x

theorem isStationary_iUnion_iff_of_countable {α : Type v} [LinearOrder α] [WellFoundedLT α] {ι : Sort u_1} {f : ι → Set α} [Countable ι] (hα : Order.cof α ≠ Cardinal.aleph0) :

IsStationary (⋃ (i : ι), f i) ↔ ∃ (i : ι), IsStationary (f i)

theorem isStationary_union_iff {α : Type v} {s t : Set α} [LinearOrder α] [WellFoundedLT α] (hα : Order.cof α ≠ Cardinal.aleph0) :

IsStationary (s ∪ t) ↔ IsStationary s ∨ IsStationary t