Ultrametric structure on continuous maps

instance ContinuousMap.isUltrametricDist {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [CompactSpace X] [MetricSpace Y] [IsUltrametricDist Y] : IsUltrametricDist C(X, Y)

Continuous maps from a compact space to an ultrametric space are an ultrametric space.