Distance Function for Distinct Elements in Metric Space is Strictly Positive

From ProofWiki
Jump to navigation Jump to search


Let $A$ be a set.

Let $d: A \times A \to \R$ be a real-valued function on $A$ with the following properties:

\((\text M 1')\)   $:$     \(\ds \forall x, y \in A:\) \(\ds \map d {x, y} = 0 \iff x = y \)      
\((\text M 2)\)   $:$     \(\ds \forall x, y, z \in A:\) \(\ds \map d {x, y} + \map d {y, z} \ge \map d {x, z} \)      
\((\text M 3)\)   $:$     \(\ds \forall x, y \in A:\) \(\ds \map d {x, y} = \map d {y, x} \)      

which can be considered as being an alternative formulation of the metric space axioms.


$\forall x, y \in A: x \ne y \implies \map d {x, y} > 0$

which is Metric Space Axiom $(\text M 4)$.

Thus $d$ is a distance function, so making $M := \struct {A, d}$ a metric space.


\(\ds \forall x, y \in A: \, \) \(\ds \map d {x, y} + \map d {y, x}\) \(\ge\) \(\ds \map d {x, x}\) from Metric Space Axiom $(\text M 2)$
\(\ds \leadsto \ \ \) \(\ds 2 \map d {x, y}\) \(\ge\) \(\ds 0\) from Axiom $(\text M 1')$ above and Metric Space Axiom $(\text M 3)$
\(\ds \leadsto \ \ \) \(\ds \map d {x, y}\) \(\ge\) \(\ds 0\)