Completions of ultrametric spaces #
The distance on the completion of a pseudometric space extends the distance on the space by
continuity, and the strong triangle inequality dist x z ≤ max (dist x y) (dist y z) is a closed
condition, so the completion of an ultrametric space is ultrametric. In particular the
completion of a nonarchimedean normed ring has an ultrametric norm.
instance
UniformSpace.Completion.instIsUltrametricDist_tauCeti
{X : Type u_1}
[PseudoMetricSpace X]
[IsUltrametricDist X]
:
The completion of an ultrametric space is ultrametric.