# Documentation

## Mathlib.SetTheory.Ordinal.Topology

### Topology of ordinals #

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

### Main results #

• Ordinal.isClosed_iff_sup / 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.
theorem Ordinal.nhdsBasis_Ioc {a : Ordinal.{u}} (h : a 0) :
Filter.HasBasis (nhds a) (fun (x : Ordinal.{u}) => x < a) fun (x : Ordinal.{u}) => Set.Ioc x a
theorem Ordinal.isOpen_iff {s : } :
os, ∃ a < o, Set.Ioo a o s
theorem Ordinal.mem_closure_tfae (a : Ordinal.{u}) (s : ) :
List.TFAE [a , a closure (s ), Set.Nonempty (s ) sSup (s ) = a, ∃ t ⊆ s, sSup t = a, ∃ (o : Ordinal.{u}), o 0 ∃ (f : (x : Ordinal.{u}) → x < oOrdinal.{u}), (∀ (x : Ordinal.{u}) (hx : x < o), f x hx s) = a, ∃ (ι : Type u), ∃ (f : ), (∀ (i : ι), f i s) = a]
theorem Ordinal.mem_closure_iff_sup {s : } {a : Ordinal.{u}} :
a ∃ (ι : Type u) (_ : ) (f : ), (∀ (i : ι), f i s) = a
theorem Ordinal.mem_closed_iff_sup {s : } {a : Ordinal.{u}} (hs : ) :
a s ∃ (ι : Type u) (_ : ) (f : ), (∀ (i : ι), f i s) = a
theorem Ordinal.mem_closure_iff_bsup {s : } {a : Ordinal.{u}} :
a ∃ (o : Ordinal.{u}) (_ : o 0) (f : (a : Ordinal.{u}) → a < oOrdinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi s) = a
theorem Ordinal.mem_closed_iff_bsup {s : } {a : Ordinal.{u}} (hs : ) :
a s ∃ (o : Ordinal.{u}) (_ : o 0) (f : (a : Ordinal.{u}) → a < oOrdinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi s) = a
theorem Ordinal.isClosed_iff_sup {s : } :
∀ {ι : Type u}, ∀ (f : ), (∀ (i : ι), f i s) s
theorem Ordinal.isClosed_iff_bsup {s : } :
∀ {o : Ordinal.{u}}, o 0∀ (f : (a : Ordinal.{u}) → a < oOrdinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi s) s
theorem Ordinal.isLimit_of_mem_frontier {s : } {a : Ordinal.{u}} (ha : a ) :
theorem Ordinal.enumOrd_isNormal_iff_isClosed {s : } (hs : Set.Unbounded (fun (x x_1 : Ordinal.{u}) => x < x_1) s) :