Documentation

Mathlib.SetTheory.Ordinal.Topology

Topology of ordinals #

We prove some miscellaneous results involving the order topology of ordinals.

Main results #

Todo #

Most things in this file should be generalized to other well-orders, or to Scott-Hausdorff topologies.

source
@[instance_reducible]
instance Ordinal.instTopologicalSpace :
TopologicalSpace Ordinal.{u}
Equations
source
instance Ordinal.instOrderTopology :
OrderTopology Ordinal.{u}
source
theorem Ordinal.mem_closure_tfae (a : Ordinal.{u}) (s : Set Ordinal.{u}) :
[a ∈ closure s, a ∈ closure (s ∩ Set.Iic a), (s ∩ Set.Iic a).Nonempty ∧ sSup (s ∩ Set.Iic a) = a, ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a, ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a].TFAE
source
theorem Ordinal.mem_closure_iff_iSup {s : Set Ordinal.{u}} {a : Ordinal.{u}} :
a ∈ closure s ↔ ∃ (ι : Type u) (_ : Nonempty ι) (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a
source
theorem Ordinal.mem_iff_iSup_of_isClosed {s : Set Ordinal.{u}} {a : Ordinal.{u}} (hs : IsClosed s) :
a ∈ s ↔ ∃ (ι : Type u) (_ : Nonempty ι) (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a
source
theorem Ordinal.isClosed_iff_iSup {s : Set Ordinal.{u}} :
IsClosed s ↔ ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ (i : ι), f i ∈ s
source
@[deprecated Order.isNormal_enum_iff_dirSupClosed (since := "2026-05-25")]
theorem Ordinal.enumOrd_isNormal_iff_isClosed {s : Set Ordinal.{u}} (hs : ¬BddAbove s) :
Order.IsNormal (enumOrd s) ↔ IsClosed s
source
@[deprecated AccPt (since := "2026-05-24")]
def Ordinal.IsAcc (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
    @[deprecated IsClosed (since := "2026-05-24")]
    def Ordinal.IsClosedBelow (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
      @[deprecated SuccOrder.accPt_principal (since := "2026-05-24")]
      theorem Ordinal.isAcc_iff (o : Ordinal.{u_1}) (S : Set Ordinal.{u_1}) :
      o.IsAcc S ↔ o ≠ 0 ∧ ∀ p < o, (S ∩ Set.Ioo p o).Nonempty
      source
      @[deprecated SuccOrder.accPt_principal (since := "2026-05-24")]
      theorem Ordinal.IsAcc.forall_lt {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}} (h : o.IsAcc S) (p : Ordinal.{u_1}) :
      p < o → (S ∩ Set.Ioo p o).Nonempty
      source
      @[deprecated AccPt.not_isMin (since := "2026-05-24")]
      theorem Ordinal.IsAcc.pos {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}} (h : o.IsAcc S) :
      0 < o
      source
      @[deprecated AccPt.isSuccLimit (since := "2026-05-24")]
      theorem Ordinal.IsAcc.isSuccLimit {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}} (h : o.IsAcc S) :
      Order.IsSuccLimit o
      source
      @[deprecated AccPt.mono (since := "2026-05-24")]
      theorem Ordinal.IsAcc.mono {o : Ordinal.{u_1}} {S T : Set Ordinal.{u_1}} (h : S ⊆ T) (ho : o.IsAcc S) :
      o.IsAcc T
      source
      @[deprecated SuccOrder.accPt_principal (since := "2026-05-24")]
      theorem Ordinal.IsAcc.inter_Ioo_nonempty {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}} (hS : o.IsAcc S) {p : Ordinal.{u_1}} (hp : p < o) :
      (S ∩ Set.Ioo p o).Nonempty
      source
      @[deprecated isClosed_iff_accPt (since := "2026-05-24")]
      theorem Ordinal.isClosedBelow_iff {S : Set Ordinal.{u_1}} {o : Ordinal.{u_1}} :
      IsClosedBelow S o ↔ ∀ p < o, p.IsAcc S → p ∈ S
      source
      @[deprecated isClosed_iff_accPt (since := "2026-05-24")]
      theorem Ordinal.IsClosedBelow.forall_lt {S : Set Ordinal.{u_1}} {o : Ordinal.{u_1}} :
      IsClosedBelow S o → ∀ p < o, p.IsAcc S → p ∈ S

      Alias of the forward direction of Ordinal.isClosedBelow_iff.

      source
      @[deprecated isClosed_sInter (since := "2026-05-24")]
      theorem Ordinal.IsClosedBelow.sInter {o : Ordinal.{u_1}} {S : Set (Set Ordinal.{u_1})} (h : ∀ C ∈ S, IsClosedBelow C o) :
      IsClosedBelow (⋂₀ S) o
      source
      @[deprecated isClosed_iInter (since := "2026-05-24")]
      theorem Ordinal.IsClosedBelow.iInter {ι : Type u} {f : ι → Set Ordinal.{u_1}} {o : Ordinal.{u_1}} (h : ∀ (i : ι), IsClosedBelow (f i) o) :
      IsClosedBelow (⋂ (i : ι), f i) o