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
@[implicit_reducible]
instance Ordinal.instTopologicalSpace :
TopologicalSpace Ordinal.{u}
Equations
source
instance Ordinal.instOrderTopology :
OrderTopology Ordinal.{u}
source
@[deprecated SuccOrder.isOpen_singleton_iff (since := "2026-01-20")]
theorem Ordinal.isOpen_singleton_iff {a : Ordinal.{u}} :
IsOpen {a} ↔ ¬Order.IsSuccLimit a
source
@[deprecated SuccOrder.nhds_eq_pure (since := "2026-01-20")]
theorem Ordinal.nhds_eq_pure {a : Ordinal.{u}} :
nhds a = pure a ↔ ¬Order.IsSuccLimit a
source
@[deprecated SuccOrder.isOpen_iff (since := "2026-01-20")]
theorem Ordinal.isOpen_iff {s : Set Ordinal.{u}} :
IsOpen s ↔ ∀ o ∈ s, Order.IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s
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
@[deprecated Ordinal.mem_closure_iff_iSup (since := "2026-04-05")]
theorem Ordinal.mem_closure_iff_bsup {s : Set Ordinal.{u}} {a : Ordinal.{u}} :
a ∈ closure s ↔ ∃ (o : Ordinal.{u}) (_ : o ≠ 0) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a
source
@[deprecated Ordinal.mem_closure_iff_iSup (since := "2026-04-05")]
theorem Ordinal.mem_closed_iff_bsup {s : Set Ordinal.{u}} {a : Ordinal.{u}} (hs : IsClosed s) :
a ∈ s ↔ ∃ (o : Ordinal.{u}) (_ : o ≠ 0) (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = 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 Ordinal.isClosed_iff_iSup (since := "2026-04-05")]
theorem Ordinal.isClosed_iff_bsup {s : Set Ordinal.{u}} :
IsClosed s ↔ ∀ {o : Ordinal.{u}}, o ≠ 0 → ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
source
@[deprecated SuccOrder.isSuccLimit_of_mem_frontier (since := "2026-01-20")]
theorem Ordinal.isSuccLimit_of_mem_frontier {s : Set Ordinal.{u}} {a : Ordinal.{u}} (ha : a ∈ frontier s) :
Order.IsSuccLimit a
source
theorem Ordinal.enumOrd_isNormal_iff_isClosed {s : Set Ordinal.{u}} (hs : ¬BddAbove s) :
Order.IsNormal (enumOrd s) ↔ IsClosed s
source
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
    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
      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
      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
      theorem Ordinal.IsAcc.pos {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}} (h : o.IsAcc S) :
      0 < o
      source
      theorem Ordinal.IsAcc.isSuccLimit {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}} (h : o.IsAcc S) :
      Order.IsSuccLimit o
      source
      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
      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 Topology.IsOpenEmbedding.accPt_comap_iff (since := "2026-03-30")]
      theorem Ordinal.accPt_subtype {p o : Ordinal.{u_1}} (S : Set Ordinal.{u_1}) (hpo : p < o) :
      AccPt p (Filter.principal S) ↔ AccPt ⟨p, hpo⟩ (Filter.principal (Subtype.val ⁻¹' S))
      source
      theorem Ordinal.isClosedBelow_iff {S : Set Ordinal.{u_1}} {o : Ordinal.{u_1}} :
      IsClosedBelow S o ↔ ∀ p < o, p.IsAcc S → p ∈ S
      source
      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
      theorem Ordinal.IsClosedBelow.sInter {o : Ordinal.{u_1}} {S : Set (Set Ordinal.{u_1})} (h : ∀ C ∈ S, IsClosedBelow C o) :
      IsClosedBelow (⋂₀ S) o
      source
      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