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

• developable : Nonempty (Development X)
• t0 ⦃x y : X⦄ : Inseparable x y → x = y
• regular {s : Set X} {a : X} : IsClosed s → a ∉ s → Disjoint (nhdsSet s) (nhds a)