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

• locally_metrizable (x : X) : ∃ C ∈ nhds x, TopologicalSpace.MetrizableSpace ↑C