Documentation

Mathlib.SetTheory.Ordinal.Topology

Topology of ordinals #

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

Main results #

theorem Ordinal.nhdsBasis_Ioc {a : Ordinal.{u}} (h : a 0) :
Filter.HasBasis (nhds a) (fun x => x < a) fun x => Set.Ioc x a
theorem Ordinal.isOpen_iff {s : Set Ordinal.{u}} :
IsOpen s ∀ (o : Ordinal.{u}), o sOrdinal.IsLimit oa, a < o Set.Ioo a o s
theorem Ordinal.mem_closure_tfae (a : Ordinal.{u}) (s : Set Ordinal.{u}) :
List.TFAE [a closure s, a closure (s Set.Iic a), Set.Nonempty (s Set.Iic a) sSup (s Set.Iic a) = a, t, t s Set.Nonempty t BddAbove t sSup t = a, o, o 0 f, (∀ (x : Ordinal.{u}) (hx : x < o), f x hx s) Ordinal.bsup o f = a, ι, Nonempty ι f, (∀ (i : ι), f i s) Ordinal.sup f = a]
theorem Ordinal.mem_closure_iff_sup {s : Set Ordinal.{u}} {a : Ordinal.{u}} :
a closure s ι x f, (∀ (i : ι), f i s) Ordinal.sup f = a
theorem Ordinal.mem_closed_iff_sup {s : Set Ordinal.{u}} {a : Ordinal.{u}} (hs : IsClosed s) :
a s ι _hι f, (∀ (i : ι), f i s) Ordinal.sup f = a
theorem Ordinal.mem_closure_iff_bsup {s : Set Ordinal.{u}} {a : Ordinal.{u}} :
a closure s o _ho f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi s) Ordinal.bsup o f = a
theorem Ordinal.mem_closed_iff_bsup {s : Set Ordinal.{u}} {a : Ordinal.{u}} (hs : IsClosed s) :
a s o _ho f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi s) Ordinal.bsup o f = a
theorem Ordinal.isClosed_iff_sup {s : Set Ordinal.{u}} :
IsClosed s ∀ {ι : Type u}, Nonempty ι∀ (f : ιOrdinal.{u}), (∀ (i : ι), f i s) → Ordinal.sup f s
theorem Ordinal.isClosed_iff_bsup {s : Set Ordinal.{u}} :
IsClosed s ∀ {o : Ordinal.{u}}, o 0∀ (f : (a : Ordinal.{u}) → a < oOrdinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi s) → Ordinal.bsup o f s