# mathlibdocumentation

set_theory.ordinal.topology

### Topology of ordinals #

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 so.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 < oordinal), (∀ (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 < oordinal), (∀ (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 < oordinal), (∀ (i : ordinal) (hi : i < o), f i hi s)o.bsup f s