Metric space
Set
| context | $X$ … set |
| definiendum | $\langle X,d\rangle\in\mathrm{it}$ |
| postulate | $d$ … metric $X$ |
We can reconstruct the set underlying a metric via $\text{dom}(\text{dom}(d))=\text{dom}(X\times X)=X$, so the set of metrics and the set of metric spaces over $X$ are in bijection.
Reference
Wikipedia: Metric space
Requirements*
Refinement of
Equivalent to
