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

• compact_t2 (s : Set X) : IsCompact s → T2Space ↑s