Topology of ordinals

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

Main results

• Ordinal.isClosed_iff_iSup / Ordinal.isClosed_iff_bsup: A set of ordinals is closed iff it's closed under suprema.
• Ordinal.isNormal_iff_strictMono_and_continuous: A characterization of normal ordinal functions.
• Ordinal.enumOrd_isNormal_iff_isClosed: The function enumerating the ordinals of a set is normal iff the set is closed.

@[implicit_reducible]

instance Ordinal.instTopologicalSpace : TopologicalSpace Ordinal.{u}

instance Ordinal.instOrderTopology : OrderTopology Ordinal.{u}

@[deprecated SuccOrder.isOpen_singleton_iff (since := "2026-01-20")]

theorem Ordinal.isOpen_singleton_iff {a : Ordinal.{u}} : IsOpen {a} ↔ ¬Order.IsSuccLimit a

@[deprecated SuccOrder.nhds_eq_pure (since := "2026-01-20")]

theorem Ordinal.nhds_eq_pure {a : Ordinal.{u}} : nhds a = pure a ↔ ¬Order.IsSuccLimit a

@[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

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, ∃ (o : Ordinal.{u}), o ≠ 0 ∧ ∃ (f : (x : Ordinal.{u}) → x < o → Ordinal.{u}), (∀ (x : Ordinal.{u}) (hx : x < o), f x hx ∈ s) ∧ o.bsup f = a, ∃ (ι : Type u), Nonempty ι ∧ ∃ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) ∧ ⨆ (i : ι), f i = a].TFAE

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

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

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

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

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

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

@[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

theorem Ordinal.enumOrd_isNormal_iff_isClosed {s : Set Ordinal.{u}} (hs : ¬BddAbove s) : Order.IsNormal (enumOrd s) ↔ IsClosed s

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.

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.

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

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

theorem Ordinal.IsAcc.pos {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}} (h : o.IsAcc S) : 0 < o

theorem Ordinal.IsAcc.isSuccLimit {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}} (h : o.IsAcc S) : Order.IsSuccLimit o

theorem Ordinal.IsAcc.mono {o : Ordinal.{u_1}} {S T : Set Ordinal.{u_1}} (h : S ⊆ T) (ho : o.IsAcc S) : o.IsAcc T

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

@[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))

theorem Ordinal.isClosedBelow_iff {S : Set Ordinal.{u_1}} {o : Ordinal.{u_1}} : IsClosedBelow S o ↔ ∀ p < o, p.IsAcc S → p ∈ S

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.

theorem Ordinal.IsClosedBelow.sInter {o : Ordinal.{u_1}} {S : Set (Set Ordinal.{u_1})} (h : ∀ C ∈ S, IsClosedBelow C o) : IsClosedBelow (⋂₀ S) o

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