Can a metric space have a distance function that maps to any arbitrary ordered field other than the set of positive Real Numbers?

112 Views Asked by At

All the definitions I've found on line for a metric space is that a Metric Space is an ordered pair (M, p) where M is a non-empty set and p is a distance function where,

$p: M \times M \rightarrow \mathbb{R} $

I was curious if this could be further generalised to the subset of all positive value in any arbitrary ordered field F, i.e.

$p : M \times M \rightarrow F^{+}$

Where $F^{+} = \{f \in F \: |\: f \geq_{F} 0_{F}\}$

With $0_{F}$ being the additive inverse for $F$ and

$\geq_{F}$ is the greater than or equal operator for $F$.

Any tips/suggestions/comments would be greatly appreciated.

Thanks, David