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

• compact_finite (s : Set X) : IsCompact s → s.Finite