class PiBase.CWGH (X : Type u) [TopologicalSpace X] extends UCompactlyGeneratedSpace X, PiBase.WeakT2Space X : Prop

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