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

• weakly_countably_compact (s : Set X) : s.Infinite → ∃ (x : X), AccPt x (Filter.principal s)