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.

Club sets

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

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.

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 α} : IsClub s

@[simp]

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

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

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) : sSup t ∈ s

theorem IsClub.ciSup_mem {α : Type u_1} [ConditionallyCompleteLinearOrder α] {ι : Sort u_2} {f : ι → α} [Nonempty ι] {s : Set α} (hs : IsClub s) (ht : Set.range f ⊆ s) (ht' : BddAbove (Set.range f)) : ⨆ (i : ι), f i ∈ s

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 IsClub.diag {α : Type v} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] {f : α → Set α} (hα : Order.cof α ≠ Cardinal.aleph0) (hf : ∀ (a : α), IsClub (f a)) : IsClub {a : α | ∀ b < a, a ∈ f b}

Club sets are closed under diagonal intersections.

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 α) : Prop

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

Equations

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

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) : IsStationary t

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

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ᶜ) : IsStationary 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) : IsStationary 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

theorem exists_isStationary_preimage_singleton {α : Type v} {s : Set α} [LinearOrder α] [WellFoundedLT α] [IsRegularCardinalOrder α] {f : α → α} (hα : Order.cof α ≠ Cardinal.aleph0) (hs : IsStationary s) (hf : ∀ x ∈ s, f x < x) : ∃ (a : α), IsStationary (s ∩ f ⁻¹' {a})

Fodor's lemma, or the pressing down lemma: if α has the order type of a regular cardinal, s is a stationary set, and f : α → α is a regressive function on s, there exists some stationary subset of s on which f is constant.