Metric spaces
Content created by malarbol, Louis Wasserman and Fredrik Bakke.
Created on 2024-09-28.
Last modified on 2025-08-18.
Idea
Metric spaces are types structured with a concept of distance on its elements.
Since we operate in a constructive setting, the concept of distance is captured
by considering upper bounds on the distance between points, rather than by a
distance function as in the classical approach. Thus, a metric space A
is
defined by a family of neighborhood
relations on it indexed by the
positive rational numbers
ℚ⁺
,
N : ℚ⁺ → A → A → Prop l
that satisfies certain axioms. Constructing a proof of N d x y
amounts to
saying that d
is an upper bound on the distance from x
to y
.
The neighborhood relation on a metric space must satisfy the following axioms:
- Reflexivity. Every positive rational
d
is an upper bound on the distance fromx
to itself. - Symmetry. If
d
is an upper bound on the distance fromx
toy
, thend
is an upper bound on the distance fromy
tox
. - Triangularity. If
d
is an upper bound on the distance fromx
toy
, andd'
is an upper bound on the distance fromy
toz
, thend + d'
is an upper bound on the distance fromx
toz
.
Finally, we ask that our metric spaces are extensional, which amounts to the property of indistinguishability of identicals
- If every positive rational
d
is an upper bound on the distance fromx
toy
, thenx
andy
are equal.
Instances of metric spaces
Metric space | File |
---|---|
Metric space of Cauchy approximations in a metric space | metric-spaces.metric-space-of-cauchy-approximations-metric-spaces |
Metric space of convergent Cauchy approximations in a metric space | metric-spaces.metric-space-of-convergent-cauchy-approximations-metric-spaces |
Metric space of rational numbers | metric-spaces.metric-space-of-rational-numbers |
Metric space of real numbers | real-numbers.metric-space-of-real-numbers |
Modules in the metric spaces namespace
module metric-spaces where open import metric-spaces.category-of-metric-spaces-and-isometries public open import metric-spaces.category-of-metric-spaces-and-short-functions public open import metric-spaces.cauchy-approximations-metric-spaces public open import metric-spaces.cauchy-approximations-pseudometric-spaces public open import metric-spaces.cauchy-sequences-complete-metric-spaces public open import metric-spaces.cauchy-sequences-metric-spaces public open import metric-spaces.complete-metric-spaces public open import metric-spaces.continuous-functions-metric-spaces public open import metric-spaces.convergent-cauchy-approximations-metric-spaces public open import metric-spaces.convergent-sequences-metric-spaces public open import metric-spaces.dependent-products-metric-spaces public open import metric-spaces.discrete-metric-spaces public open import metric-spaces.elements-at-bounded-distance-metric-spaces public open import metric-spaces.equality-of-metric-spaces public open import metric-spaces.equality-of-pseudometric-spaces public open import metric-spaces.extensionality-pseudometric-spaces public open import metric-spaces.functions-metric-spaces public open import metric-spaces.functions-pseudometric-spaces public open import metric-spaces.functor-category-set-functions-isometry-metric-spaces public open import metric-spaces.functor-category-short-isometry-metric-spaces public open import metric-spaces.indexed-sums-metric-spaces public open import metric-spaces.isometries-metric-spaces public open import metric-spaces.isometries-pseudometric-spaces public open import metric-spaces.limits-of-cauchy-approximations-metric-spaces public open import metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces public open import metric-spaces.limits-of-functions-metric-spaces public open import metric-spaces.limits-of-sequences-metric-spaces public open import metric-spaces.lipschitz-functions-metric-spaces public open import metric-spaces.locally-constant-functions-metric-spaces public open import metric-spaces.metric-space-of-cauchy-approximations-complete-metric-spaces public open import metric-spaces.metric-space-of-cauchy-approximations-metric-spaces public open import metric-spaces.metric-space-of-convergent-cauchy-approximations-metric-spaces public open import metric-spaces.metric-space-of-convergent-sequences-metric-spaces public open import metric-spaces.metric-space-of-functions-metric-spaces public open import metric-spaces.metric-space-of-isometries-metric-spaces public open import metric-spaces.metric-space-of-lipschitz-functions-metric-spaces public open import metric-spaces.metric-space-of-rational-numbers public open import metric-spaces.metric-space-of-short-functions-metric-spaces public open import metric-spaces.metric-spaces public open import metric-spaces.monotonic-rational-neighborhood-relations public open import metric-spaces.poset-of-rational-neighborhood-relations public open import metric-spaces.precategory-of-metric-spaces-and-functions public open import metric-spaces.precategory-of-metric-spaces-and-isometries public open import metric-spaces.precategory-of-metric-spaces-and-short-functions public open import metric-spaces.preimages-rational-neighborhood-relations public open import metric-spaces.pseudometric-spaces public open import metric-spaces.rational-approximations-of-zero public open import metric-spaces.rational-cauchy-approximations public open import metric-spaces.rational-neighborhood-relations public open import metric-spaces.rational-sequences-approximating-zero public open import metric-spaces.reflexive-rational-neighborhood-relations public open import metric-spaces.saturated-rational-neighborhood-relations public open import metric-spaces.sequences-metric-spaces public open import metric-spaces.short-functions-metric-spaces public open import metric-spaces.short-functions-pseudometric-spaces public open import metric-spaces.similarity-of-elements-pseudometric-spaces public open import metric-spaces.subspaces-metric-spaces public open import metric-spaces.symmetric-rational-neighborhood-relations public open import metric-spaces.triangular-rational-neighborhood-relations public open import metric-spaces.uniformly-continuous-functions-metric-spaces public
References
Our setup for metric space theory closely follows [Boo20].
- [Boo20]
- Auke Bart Booij. Analysis in univalent type theory. PhD thesis, University of Birmingham, 2020. URL: https://etheses.bham.ac.uk/id/eprint/10411/7/Booij20PhD.pdf.
Recent changes
- 2025-08-18. malarbol and Louis Wasserman. Refactor metric spaces (#1450).
- 2025-05-27. malarbol. Zero approximations (#1424).
- 2025-05-19. malarbol. Lipschitz-continuous functions between metric spaces (#1417).
- 2025-05-05. malarbol. Metric properties of real negation, absolute value, addition and maximum (#1398).
- 2025-05-01. malarbol. Limits of sequences in metric spaces (#1378).