class PiBase.CosmicSpace (X : Type u_1) [TopologicalSpace X] extends T3Space X, PiBase.HasCountableNetwork X : Prop

• t0 ⦃x y : X⦄ : Inseparable x y → x = y
• regular {s : Set X} {a : X} : IsClosed s → a ∉ s → Disjoint (nhdsSet s) (nhds a)
• has_countable_network : ∃ (ι : Type) (f : ι → Set X), Countable ι ∧ IsNetwork f