Documentation

LeanPool.PCFTheory.Background.Topology

Topological results on ordinals #

A handful of order-topological facts used to set up the theory of clubs.

Accumulation points and closed-below sets #

Mathlib's Ordinal.IsAcc/Ordinal.IsClosedBelow were deprecated in favour of the generic topological AccPt/IsClosed. We keep working with the ordinal-specific phrasing through these local replacements, defined exactly as the former Mathlib declarations together with the small API the rest of the development relies on.

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

An ordinal is an accumulation point of a set of ordinals if it is positive and there are elements in the set arbitrarily close to the ordinal from below.

Equations
Instances For
    source
    def Ordinal.IsClosedBelowPt (S : Set Ordinal.{u_1}) (o : Ordinal.{u_1}) :
    Prop

    A set of ordinals is closed below an ordinal if it contains all of its accumulation points below the ordinal.

    Equations
    Instances For
      source
      theorem Ordinal.isAccPt_iff (o : Ordinal.{u_1}) (S : Set Ordinal.{u_1}) :
      o.IsAccPt S ↔ o ≠ 0 ∧ ∀ p < o, (S ∩ Set.Ioo p o).Nonempty
      source
      theorem Ordinal.IsAccPt.forall_lt {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}} (h : o.IsAccPt S) (p : Ordinal.{u_1}) :
      p < o → (S ∩ Set.Ioo p o).Nonempty
      source
      theorem Ordinal.IsAccPt.pos {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}} (h : o.IsAccPt S) :
      0 < o
      source
      theorem Ordinal.IsAccPt.isSuccLimit {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}} (h : o.IsAccPt S) :
      Order.IsSuccLimit o
      source
      theorem Ordinal.IsAccPt.mono {o : Ordinal.{u_1}} {S T : Set Ordinal.{u_1}} (h : S ⊆ T) (ho : o.IsAccPt S) :
      o.IsAccPt T
      source
      theorem Ordinal.IsAccPt.inter_Ioo_nonempty {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}} (hS : o.IsAccPt S) {p : Ordinal.{u_1}} (hp : p < o) :
      (S ∩ Set.Ioo p o).Nonempty
      source
      theorem Ordinal.isClosedBelowPt_iff {S : Set Ordinal.{u_1}} {o : Ordinal.{u_1}} :
      IsClosedBelowPt S o ↔ ∀ p < o, p.IsAccPt S → p ∈ S
      source
      theorem Ordinal.IsClosedBelowPt.forall_lt {S : Set Ordinal.{u_1}} {o : Ordinal.{u_1}} (h : IsClosedBelowPt S o) (p : Ordinal.{u_1}) :
      p < o → p.IsAccPt S → p ∈ S
      source
      theorem Ordinal.IsClosedBelowPt.sInter {o : Ordinal.{u_1}} {S : Set (Set Ordinal.{u_1})} (h : ∀ C ∈ S, IsClosedBelowPt C o) :
      IsClosedBelowPt (⋂₀ S) o
      source
      instance Ordinal.instSmallElemIio_leanPool {o : Ordinal.{u}} :
      Small.{max u v, u + 1} ↑(Set.Iio o)
      source
      theorem Ordinal.instNoMaxOrderIio {o : Ordinal.{u_1}} (h : Order.IsSuccLimit o) :
      NoMaxOrder ↑(Set.Iio o)

      If o is a successor limit, Iio o has no maximal element.

      source
      theorem Ordinal.IsAccPt.inter_Ioi {o p : Ordinal.{u_1}} {S : Set Ordinal.{u_1}} (h : o.IsAccPt S) (hp : p < o) :
      o.IsAccPt (S ∩ Set.Ioi p)
      source
      theorem Ordinal.isAccPt_iSup {o : Ordinal.{u}} {α : ↑(Set.Iio o)} (ho : Order.IsSuccLimit o) (f : ↑(Set.Iio o) → Ordinal.{v}) [Small.{v, u + 1} ↑(Set.Iio o)] (hf : ∀ (α β : ↑(Set.Iio o)), α < β → f α < f β) {S : Set Ordinal.{v}} (hp : ∀ (β : ↑(Set.Iio o)), α < β → f β ∈ S) :
      (iSup f).IsAccPt S
      source
      theorem Ordinal.mk_derivedSet_le (S : Set Ordinal.{u_1}) :
      Cardinal.mk ↑(derivedSet S) ≤ Cardinal.mk ↑S
      source
      theorem Ordinal.isClosedBelowPt_derivedSet {S : Set Ordinal.{u_1}} (o : Ordinal.{u_1}) :
      IsClosedBelowPt (S ∪ derivedSet S) o