Metric spaces

Content created by Louis Wasserman, malarbol and Fredrik Bakke.

Created on 2024-09-28.
Last modified on 2025-09-11.

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 from x to itself.
  • Symmetry. If d is an upper bound on the distance from x to y, then d is an upper bound on the distance from y to x.
  • Triangularity. If d is an upper bound on the distance from x to y, and d' is an upper bound on the distance from y to z, then d + d' is an upper bound on the distance from x to z.

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 from x to y, then x and y are equal.

Instances of metric spaces

Metric spaceFile
Metric space of Cauchy approximations in a metric spacemetric-spaces.metric-space-of-cauchy-approximations-metric-spaces
Metric space of convergent Cauchy approximations in a metric spacemetric-spaces.metric-space-of-convergent-cauchy-approximations-metric-spaces
Metric space of rational numbersmetric-spaces.metric-space-of-rational-numbers
Metric space of real numbersreal-numbers.metric-space-of-real-numbers

Modules in the metric spaces namespace

module metric-spaces where

open import metric-spaces.approximations-located-metric-spaces public
open import metric-spaces.approximations-metric-spaces public
open import metric-spaces.bounded-distance-decompositions-of-metric-spaces public
open import metric-spaces.cartesian-products-metric-spaces public
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.closed-subsets-located-metric-spaces public
open import metric-spaces.closed-subsets-metric-spaces public
open import metric-spaces.closure-subsets-metric-spaces public
open import metric-spaces.compact-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.dense-subsets-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.images-isometries-metric-spaces public
open import metric-spaces.images-metric-spaces public
open import metric-spaces.images-short-functions-metric-spaces public
open import metric-spaces.images-uniformly-continuous-functions-metric-spaces public
open import metric-spaces.indexed-sums-metric-spaces public
open import metric-spaces.inhabited-totally-bounded-subspaces-metric-spaces public
open import metric-spaces.interior-subsets-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.located-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.metrics public
open import metric-spaces.metrics-of-metric-spaces public
open import metric-spaces.metrics-of-metric-spaces-are-uniformly-continuous public
open import metric-spaces.monotonic-rational-neighborhood-relations public
open import metric-spaces.nets-located-metric-spaces public
open import metric-spaces.nets-metric-spaces public
open import metric-spaces.open-subsets-located-metric-spaces public
open import metric-spaces.open-subsets-metric-spaces 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.totally-bounded-metric-spaces public
open import metric-spaces.totally-bounded-subspaces-metric-spaces 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