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

• ex_ultrametric : ∃ (t : MetricSpace X), IsUltrametricDist X ∧ PseudoMetricSpace.toUniformSpace.toTopologicalSpace = τ