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

• compact_closed {K : Type u} (x✝ : TopologicalSpace K) ⦃f : K → X⦄ : Continuous f → CompactSpace K → T2Space K → IsClosed (Set.range f)