metric_space

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.

Metric space

Set

Reference

Requirements*

Refinement of

Equivalent to