# mathlib3documentation

set_theory.ordinal.topology

### Topology of ordinals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

### Main results #

• ordinal.is_closed_iff_sup / ordinal.is_closed_iff_bsup: A set of ordinals is closed iff it's closed under suprema.
• ordinal.is_normal_iff_strict_mono_and_continuous: A characterization of normal ordinal functions.
• ordinal.enum_ord_is_normal_iff_is_closed: The function enumerating the ordinals of a set is normal iff the set is closed.
@[protected, instance]
Equations
@[protected, instance]
theorem ordinal.is_open_iff {s : set ordinal} :
(o : ordinal), o s o.is_limit ( (a : ordinal) (H : a < o), o s)
theorem ordinal.mem_closure_iff_sup {s : set ordinal} {a : ordinal} :
a {ι : Type u} [_inst_1 : nonempty ι] (f : ι ordinal), ( (i : ι), f i s) = a
theorem ordinal.mem_closed_iff_sup {s : set ordinal} {a : ordinal} (hs : is_closed s) :
a s {ι : Type u} (hι : nonempty ι) (f : ι ordinal), ( (i : ι), f i s) = a
theorem ordinal.mem_closure_iff_bsup {s : set ordinal} {a : ordinal} :
a {o : ordinal} (ho : o 0) (f : Π (a : ordinal), a < o ordinal), ( (i : ordinal) (hi : i < o), f i hi s) o.bsup f = a
theorem ordinal.mem_closed_iff_bsup {s : set ordinal} {a : ordinal} (hs : is_closed s) :
a s {o : ordinal} (ho : o 0) (f : Π (a : ordinal), a < o ordinal), ( (i : ordinal) (hi : i < o), f i hi s) o.bsup f = a
theorem ordinal.is_closed_iff_sup {s : set ordinal} :
{ι : Type u}, (f : ι ordinal), ( (i : ι), f i s) s
theorem ordinal.is_closed_iff_bsup {s : set ordinal} :
{o : ordinal}, o 0 (f : Π (a : ordinal), a < o ordinal), ( (i : ordinal) (hi : i < o), f i hi s) o.bsup f s