Metric spaces

Content created by Louis Wasserman, malarbol and Fredrik Bakke.

Created on 2024-09-28.
Last modified on 2025-10-26.

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.

The relationship to a real-valued distance function, called a metric, can be recovered if and only if every element of the metric space is at bounded distance from every other element, and the metric space is located, that is, for every positive rational d₁ and d₂ with d₁ < d₂, and every element x and y of the metric space, N d₂ x y or not N d₁ x y.

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-pseudocompletion-of-metric-spaces public
open import metric-spaces.cauchy-pseudocompletion-of-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.modulated-uniformly-continuous-functions-metric-spaces 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