mathlib3 documentation

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 #

@[protected, instance]
theorem ordinal.is_open_iff {s : set ordinal} :
is_open s (o : ordinal), o s o.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 < 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} :
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 < o ordinal), ( (i : ordinal) (hi : i < o), f i hi s) o.bsup f s