class PiBase.AlephZeroSpace (X : Type u) [TopologicalSpace X] extends T3Space X, PiBase.HasCountableKNetwork 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)
• ex_network : ∃ (ι : Type) (f : ι → Set X), Countable ι ∧ IsKNetwork f