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

• ex_coarser_metrizable_separable : ∃ (m : MetricSpace X), τ ≤ PseudoMetricSpace.toUniformSpace.toTopologicalSpace ∧ TopologicalSpace.SeparableSpace X