mathlib documentation

set_theory.ordinal.topology

Topology of ordinals #

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

Main results #

@[protected, instance]
theorem ordinal.is_open_iff {s : set ordinal} :
is_open s ∀ (o : ordinal), o so.is_limit(∃ (a : ordinal) (H : a < o), set.Ioo a o s)
theorem ordinal.mem_closure_iff_sup {s : set ordinal} {a : ordinal} :
a closure s ∃ {ι : Type u} [_inst_1 : nonempty ι] (f : ι → ordinal), (∀ (i : ι), f i s) ordinal.sup f = 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) ordinal.sup f = a
theorem ordinal.mem_closure_iff_bsup {s : set ordinal} {a : ordinal} :
a closure 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.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} :
is_closed s ∀ {ι : Type u}, nonempty ι∀ (f : ι → ordinal), (∀ (i : ι), f i s)ordinal.sup f s
theorem ordinal.is_closed_iff_bsup {s : set ordinal} :
is_closed s ∀ {o : ordinal}, o 0∀ (f : Π (a : ordinal), a < oordinal), (∀ (i : ordinal) (hi : i < o), f i hi s)o.bsup f s