class PiBase.SigmaSpace (X : Type u) [TopologicalSpace X] extends T3Space X, PiBase.HasSigmaLocallyFiniteNetwork 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 u) (f : ι → Set X), Sigma (fun {α : Type u} => LocallyFinite) f ∧ IsNetwork f