Club and stationary sets

This file sets up the basic theory of clubs (closed and unbounded sets) and stationary sets.

Main definitions

• Ordinal.IsClosed: A set of ordinals S is closed in o if S ⊆ Iio o and S contains every x < o such that x.IsAcc S.
• Ordinal.IsClub: A set of ordinals S is a club in o if it is closed in o and unbounded in o.

Main results

• isClub_sInter: The intersection of fewer than o.cof clubs in o is a club in o.

def Ordinal.IsClub (C : Set Ordinal.{u_1}) (o : Ordinal.{u_1}) : Prop

A set of ordinals is a club below an ordinal if it is closed and unbounded in it.

Equations

• Ordinal.IsClub C o = (Ordinal.IsClosedBelowPt C o ∧ o.IsAccPt C)

structure Ordinal.Club (α : Ordinal.{u_1}) : Type (u_1 + 1)

A club below an ordinal α is a bundled IsClub set: closed and unbounded.

• carrier : Set Ordinal.{u_1}

  The underlying set of ordinals.

• isClub : IsClub self.carrier α

  The proof that the carrier is a club below α.

@[implicit_reducible]

instance Ordinal.instSetLikeClub {α : Ordinal.{u_1}} : SetLike α.Club Ordinal.{u_1}

Equations

• Ordinal.instSetLikeClub = { coe := Ordinal.Club.carrier, coe_injective := ⋯ }

@[implicit_reducible]

instance Ordinal.instHasSubsetClub {α : Ordinal.{u_1}} : HasSubset α.Club

Equations

• Ordinal.instHasSubsetClub = { Subset := fun (C D : α.Club) => C.carrier ⊆ D.carrier }

@[implicit_reducible]

instance Ordinal.instHasSSubsetClub {α : Ordinal.{u_1}} : HasSSubset α.Club

Equations

• Ordinal.instHasSSubsetClub = { SSubset := fun (C D : α.Club) => C.carrier ⊂ D.carrier }

instance Ordinal.instIsNonstrictStrictOrderClubSubsetSSubset {α : Ordinal.{u_1}} : IsNonstrictStrictOrder α.Club (fun (x1 x2 : α.Club) => x1 ⊆ x2) fun (x1 x2 : α.Club) => x1 ⊂ x2

instance Ordinal.instAntisymmClubSubset {α : Ordinal.{u_1}} : Std.Antisymm fun (x1 x2 : α.Club) => x1 ⊆ x2

theorem Ordinal.isClub_iff {C : Set Ordinal.{u_1}} {o : Ordinal.{u_1}} : IsClub C o ↔ (∀ p < o, p.IsAccPt C → p ∈ C) ∧ o ≠ 0 ∧ ∀ p < o, (C ∩ Set.Ioo p o).Nonempty

theorem Ordinal.IsClub.isClosedBelowPt {C : Set Ordinal.{u_1}} {o : Ordinal.{u_1}} (h : IsClub C o) : IsClosedBelowPt C o

theorem Ordinal.IsClub.isAcc {C : Set Ordinal.{u_1}} {o : Ordinal.{u_1}} (h : IsClub C o) : o.IsAccPt C

theorem Ordinal.IsClub.pos {C : Set Ordinal.{u_1}} {o : Ordinal.{u_1}} (h : IsClub C o) : 0 < o

theorem Ordinal.IsClub.ne_zero {C : Set Ordinal.{u_1}} {o : Ordinal.{u_1}} {h : IsClub C o} : o ≠ 0

theorem Ordinal.IsClub.mem_of_isAcc {C : Set Ordinal.{u_1}} {o p : Ordinal.{u_1}} (h : IsClub C o) (hp : p < o) : p.IsAccPt C → p ∈ C

theorem Ordinal.IsClub.forall_lt {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}} (h : IsClub S o) (p : Ordinal.{u_1}) : p < o → (S ∩ Set.Ioo p o).Nonempty

theorem Ordinal.IsClub.inter_Iio {C : Set Ordinal.{u_1}} {o : Ordinal.{u_1}} (h : IsClub C o) : IsClub (C ∩ Set.Iio o) o

theorem Ordinal.isClub_univ {α : Ordinal.{u_1}} (h : Order.IsSuccLimit α) : IsClub Set.univ α

def Ordinal.univClub {α : Ordinal.{u_1}} (h : Order.IsSuccLimit α) : α.Club

The trivial club consisting of every ordinal below a successor-limit α.

Equations

• Ordinal.univClub h = { carrier := Set.univ, isClub := ⋯ }

theorem Ordinal.IsClub.isClub_of_isAcc {α β : Ordinal.{u_1}} {C : Set Ordinal.{u_1}} (h : β < α) (hC : IsClub C α) (hacc : β.IsAccPt C) : IsClub C β

theorem Ordinal.exists_above_of_lt_cof {o : Ordinal.{u}} {S : Set (Set Ordinal.{u})} {p : Ordinal.{u}} (h : p < o) (hSemp : Nonempty ↑S) (hSacc : ∀ U ∈ S, o.IsAccPt U) (hScard : Cardinal.mk ↑S < Cardinal.lift.{u + 1, u} o.cof) : ∃ q < o, p < q ∧ ∀ U ∈ S, (U ∩ Set.Ioo p q).Nonempty

Given less than o.cof unbounded sets in o and some q < o, there is a q < p < o such that Ioo q p contains an element of every unbounded set.

theorem Ordinal.exists_omega0_seq_succ_prop {o : Ordinal.{u}} (opos : 0 < o) {P : Ordinal.{u} → Ordinal.{u} → Prop} (hP : ∀ (p : ↑(Set.Iio o)), ∃ (q : ↑(Set.Iio o)), p < q ∧ P ↑p ↑q) (r : ↑(Set.Iio o)) : ∃ (f : ↑(Set.Iio omega0) → ↑(Set.Iio o)), (∀ (i : ↑(Set.Iio omega0)), P ↑(f i) ↑(f (Order.succ i))) ∧ (∀ (i j : ↑(Set.Iio omega0)), i < j → f i < f j) ∧ r < f ⟨0, omega0_pos⟩

Given a limit ordinal o and a property on pairs of ordinals P, such that for any p < o there is a q < o above p so that P p q, we can construct an increasing ω-sequence below o that satisfies P between every 2 consecutive elements. Additionaly, the sequence can begin arbitrarily high in o. That is, above any r < o.

theorem Ordinal.isAccPt_iSup_of_between {δ : Ordinal.{u}} (C : Set Ordinal.{max u v}) (δLim : Order.IsSuccLimit δ) (s : ↑(Set.Iio δ) → Ordinal.{max u v}) (sInc : ∀ (o : ↑(Set.Iio δ)), s o < s (Order.succ o)) (h : ∀ (o : ↑(Set.Iio δ)), (C ∩ Set.Icc (s o) (s (Order.succ o))).Nonempty) : (iSup s).IsAccPt C

If between every 2 consecutive elements of a weakly increasing δ-sequence there is an element of C, and δ is a limit ordinal, then the supremum of the sequence is an accumulation point of C.

theorem Ordinal.IsClub.sInter {o : Ordinal.{u}} {S : Set (Set Ordinal.{u})} (hCof : Cardinal.aleph0 < o.cof) (hS : ∀ C ∈ S, IsClub C o) (hSemp : S.Nonempty) (Scard : Cardinal.mk ↑S < Cardinal.lift.{u + 1, u} o.cof) : IsClub (⋂₀ S) o

The intersection of less than o.cof clubs in o is a club in o.

theorem Ordinal.IsClub.iInter_lift {o : Ordinal.{u}} {ι : Type v} {f : ι → Set Ordinal.{u}} [Nonempty ι] (hCof : Cardinal.aleph0 < o.cof) (hf : ∀ (i : ι), IsClub (f i) o) (ιCard : Cardinal.lift.{u, v} (Cardinal.mk ι) < Cardinal.lift.{v, u} o.cof) : IsClub (⋂ (i : ι), f i) o

theorem Ordinal.IsClub.iInter {o : Ordinal.{u}} {ι : Type u} {f : ι → Set Ordinal.{u}} [Nonempty ι] (hCof : Cardinal.aleph0 < o.cof) (hf : ∀ (i : ι), IsClub (f i) o) (ιCard : Cardinal.mk ι < o.cof) : IsClub (⋂ (i : ι), f i) o

theorem Ordinal.IsClub.inter {Ϟ : Ordinal.{u}} (hCof : Cardinal.aleph0 < Ϟ.cof) {C D : Set Ordinal.{u}} (hC : IsClub C Ϟ) (hD : IsClub D Ϟ) : IsClub (C ∩ D) Ϟ

theorem Ordinal.IsClub.iInter_Iio {Ϟ o : Ordinal.{u}} {p : ↑(Set.Iio o)} {f : ↑(Set.Iio p) → Set Ordinal.{u}} (hϞ : Cardinal.aleph0 < Ϟ.cof) (h : (↑p).card < Ϟ.cof) (hf : ∀ (x : ↑(Set.Iio p)), IsClub (f x) Ϟ) : IsClub (⋂ (α : ↑(Set.Iio p)), f α) Ϟ

theorem Ordinal.IsClub.derivedSet {α : Ordinal.{u}} {C : Set Ordinal.{u}} (hcof : Cardinal.aleph0 < α.cof) (h : IsClub C α) : IsClub (_root_.derivedSet C) α

Accumulation points of a club form a club.

theorem Ordinal.exists_unbounded_Iio_cof {α : Ordinal.{u}} (hlim : Order.IsSuccLimit α) : ∃ S ⊆ Set.Iio α, α.IsAccPt S ∧ Cardinal.mk ↑S = Cardinal.lift.{u + 1, u} α.cof

theorem Ordinal.exists_club_card {o : Ordinal.{u}} (h : Order.IsSuccLimit o) : ∃ (C : o.Club), Cardinal.mk ↥C = Cardinal.lift.{u + 1, u} o.cof

def Ordinal.IsStationary (S : Set Ordinal.{u_1}) (o : Ordinal.{u_1}) : Prop

A set of ordinals is stationary below an ordinal if it intersects every club of it.

Equations

• Ordinal.IsStationary S o = ∀ (C : Set Ordinal.{?u.1}), Ordinal.IsClub C o → (S ∩ C).Nonempty

theorem Ordinal.IsStationary.inter_Iio {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}} (hS : IsStationary S o) : IsStationary (S ∩ Set.Iio o) o

theorem Ordinal.IsStationary.inter_isClub {o : Ordinal.{u_1}} {S C : Set Ordinal.{u_1}} (hS : IsStationary S o) (hC : IsClub C o) : (S ∩ C ∩ Set.Iio o).Nonempty