Ultrametric structure on bounded continuous functions

The sup distance on bounded continuous functions α →ᵇ β into an ultrametric space β is ultrametric, and so is the induced distance on the space C₀(α, β) of continuous functions vanishing at infinity. This complements Mathlib's instance for C(X, Y) with X compact. In particular, for a nonarchimedean normed ring R and a discrete index I, the model space C₀(I, R) of nonarchimedean functional analysis has an ultrametric norm.

instance BoundedContinuousFunction.instIsUltrametricDist {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [PseudoMetricSpace β] [IsUltrametricDist β] : IsUltrametricDist (BoundedContinuousFunction α β)

The sup distance on bounded continuous functions into an ultrametric space is ultrametric.

instance ZeroAtInftyContinuousMap.instIsUltrametricDist {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [PseudoMetricSpace β] [Zero β] [IsUltrametricDist β] : IsUltrametricDist (ZeroAtInftyContinuousMap α β)

The sup distance on continuous functions vanishing at infinity with values in an ultrametric space is ultrametric.