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

• collectionwise_normal {ι : Type u} (F : ι → Set X) : IsDiscreteFamily F → (∀ (i : ι), IsClosed (F i)) → ∃ (U : ι → Set X), Set.univ.PairwiseDisjoint U ∧ (∀ (i : ι), IsOpen (U i)) ∧ ∀ (i : ι), F i ⊆ U i