Definition and Elementary Properties of Ultrametric Spaces

An ultrametric space is a metric space in which the triangle inequality is strengthened by using the maximum instead of the sum. More formally, such a space is equipped with a real-valued application $dist$, called distance, verifying the four following conditions. \begin{align*} & dist \ x \ y \ge 0\\ & dist \ x \ y = dist \ y \ x\\ & dist \ x \ y = 0 \longleftrightarrow x = y\\ & dist \ x \ z \le max \ (dist \ x \ y) \ (dist \ y \ z) \end{align*} In this entry, we present an elementary formalization of these spaces relying on axiomatic type classes. The connection with standard metric spaces is obtained through a subclass relationship, and fundamental properties of ultrametric spaces are formally established.