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

• countably_tight (x : X) (A : Set X) : x ∈ closure A → ∃ (D : Set X), D.Countable ∧ D ⊆ A ∧ x ∈ closure D