class PiBase.CollectionwiseHausdorffSpace (X : Type u) [TopologicalSpace X] : Prop

• collectionwise_hausdorff (u : Set X) : IsClosed u → IsDiscrete u → ∃ (s : Set (Set X)), (∀ a ∈ s, IsOpen a) ∧ (∀ a ∈ s, ∀ b ∈ s, a ≠ b → Disjoint a b) ∧ (∀ x ∈ u, ∃ a ∈ s, x ∈ a) ∧ ∀ a ∈ s, ∃! x : X, x ∈ u ∧ x ∈ a