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

• kc (s : Set X) : IsCompact s → IsClosed s