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

• ex_regular_open : Pairwise fun (x y : X) => ∃ (s : Set X), IsRegularOpen s ∧ x ∈ s ∧ y ∉ s