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

• locally_finite (x : X) : ∃ s ∈ nhds x, s.Finite