X : Type u_1
inst✝² : UniformSpace X
inst✝¹ : IsCountablyGenerated (𝓤 X)
inst✝ : T0Space X
this : MetricSpace X := UniformSpace.metricSpace X
⊢ TopologicalSpace.MetrizableSpace X
X : Type u_1
inst✝² : UniformSpace X
inst✝¹ : IsCountablyGenerated (𝓤 X)
inst✝ : T0Space X
⊢ TopologicalSpace.MetrizableSpace X
letI := UniformSpace.metricSpace X
no goals
X : Type u_1
inst✝² : UniformSpace X
inst✝¹ : IsCountablyGenerated (𝓤 X)
inst✝ : T0Space X
this : MetricSpace X := UniformSpace.metricSpace X
⊢ TopologicalSpace.MetrizableSpace X
infer_instance