class PiBase.LocallyPseudoMetrizableSpace (X : Type u) [TopologicalSpace X] : Prop

• nbhd_pseudometrizable (x : X) : ∃ s ∈ nhds x, TopologicalSpace.PseudoMetrizableSpace ↑s