class PiBase.DowkerSpace (X : Type u) [TopologicalSpace X] extends T4Space X : Prop

• t1 (x : X) : IsClosed {x}
• normal (s t : Set X) : IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds s t
• not_countably_paracompact : ¬CountablyParacompactSpace X