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

• locally_countable (x : X) : ∃ s ∈ nhds x, s.Countable