class PiBase.OrdinalSpace (X : Type u) [TopologicalSpace X] : Prop

• homeo_ordinal : ∃ (a : Ordinal.{u}), IsHomeo X ↑(Set.Iio a)