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

• le_metrizable : ∃ (m : MetricSpace X), τ ≤ PseudoMetricSpace.toUniformSpace.toTopologicalSpace