class PiBase.StronglyCollectionwiseNormalSpace (X : Type u_1) [TopologicalSpace X] : Prop

• subset_diagonal {s : Set (X × X)} (ds : Set.diagonal X ⊆ s) (hs : IsOpen s) : ∃ (t : Set (X × X)), Set.diagonal X ⊆ t ∧ IsOpen t ∧ SetRel.comp t t ⊆ s