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

• functionally_t2 : Pairwise fun (x y : X) => ∃ (f : C(X, ↑unitInterval)), f x = 0 ∧ f y = 1