Cauchy approximations in metric spaces
Content created by malarbol, Fredrik Bakke and Louis Wasserman.
Created on 2024-09-28.
Last modified on 2025-08-18.
module metric-spaces.cauchy-approximations-metric-spaces where
Imports
open import elementary-number-theory.positive-rational-numbers open import foundation.constant-maps open import foundation.dependent-pair-types open import foundation.function-extensionality open import foundation.function-types open import foundation.homotopies open import foundation.identity-types open import foundation.propositions open import foundation.subtypes open import foundation.universe-levels open import metric-spaces.cauchy-approximations-pseudometric-spaces open import metric-spaces.metric-spaces open import metric-spaces.short-functions-metric-spaces
Idea
A
Cauchy approximation¶
in a metric space A
is a
Cauchy approximation
in its underlying pseudometric space: a
map f
from ℚ⁺
to
the carrier type of A
such that for all positive rationals ε
and δ
, f ε
and f δ
are in a
(ε + δ
)-neighborhood,
i.e., the distance between f ε
and f δ
is bounded by ε + δ
.
Definitions
Cauchy approximations in metric spaces
module _ {l1 l2 : Level} (A : Metric-Space l1 l2) where is-cauchy-approximation-prop-Metric-Space : (ℚ⁺ → type-Metric-Space A) → Prop l2 is-cauchy-approximation-prop-Metric-Space = is-cauchy-approximation-prop-Pseudometric-Space ( pseudometric-Metric-Space A) is-cauchy-approximation-Metric-Space : (ℚ⁺ → type-Metric-Space A) → UU l2 is-cauchy-approximation-Metric-Space = type-Prop ∘ is-cauchy-approximation-prop-Metric-Space cauchy-approximation-Metric-Space : UU (l1 ⊔ l2) cauchy-approximation-Metric-Space = type-subtype is-cauchy-approximation-prop-Metric-Space
module _ {l1 l2 : Level} (A : Metric-Space l1 l2) (f : cauchy-approximation-Metric-Space A) where map-cauchy-approximation-Metric-Space : ℚ⁺ → type-Metric-Space A map-cauchy-approximation-Metric-Space = map-cauchy-approximation-Pseudometric-Space ( pseudometric-Metric-Space A) ( f) is-cauchy-approximation-map-cauchy-approximation-Metric-Space : (ε δ : ℚ⁺) → neighborhood-Metric-Space ( A) ( ε +ℚ⁺ δ) ( map-cauchy-approximation-Metric-Space ε) ( map-cauchy-approximation-Metric-Space δ) is-cauchy-approximation-map-cauchy-approximation-Metric-Space = is-cauchy-approximation-map-cauchy-approximation-Pseudometric-Space ( pseudometric-Metric-Space A) ( f)
Properties
Constant maps in metric spaces are Cauchy approximations
module _ {l1 l2 : Level} (A : Metric-Space l1 l2) (x : type-Metric-Space A) where const-cauchy-approximation-Metric-Space : cauchy-approximation-Metric-Space A const-cauchy-approximation-Metric-Space = const-cauchy-approximation-Pseudometric-Space ( pseudometric-Metric-Space A) ( x)
The action of short maps on Cauchy approximations
module _ {l1 l2 l1' l2' : Level} (A : Metric-Space l1 l2) (B : Metric-Space l1' l2') (f : short-function-Metric-Space A B) where map-short-function-cauchy-approximation-Metric-Space : cauchy-approximation-Metric-Space A → cauchy-approximation-Metric-Space B map-short-function-cauchy-approximation-Metric-Space = map-short-function-cauchy-approximation-Pseudometric-Space ( pseudometric-Metric-Space A) ( pseudometric-Metric-Space B) ( f) module _ {l1 l2 : Level} (A : Metric-Space l1 l2) where eq-id-map-short-function-cauchy-approximation-Metric-Space : map-short-function-cauchy-approximation-Metric-Space ( A) ( A) ( short-id-Metric-Space A) = id eq-id-map-short-function-cauchy-approximation-Metric-Space = refl module _ {l1a l2a l1b l2b l1c l2c : Level} (A : Metric-Space l1a l2a) (B : Metric-Space l1b l2b) (C : Metric-Space l1c l2c) (g : short-function-Metric-Space B C) (f : short-function-Metric-Space A B) where eq-comp-map-short-function-cauchy-approximation-Metric-Space : ( map-short-function-cauchy-approximation-Metric-Space B C g ∘ map-short-function-cauchy-approximation-Metric-Space A B f) = ( map-short-function-cauchy-approximation-Metric-Space A C (comp-short-function-Metric-Space A B C g f)) eq-comp-map-short-function-cauchy-approximation-Metric-Space = refl
Homotopic Cauchy approximations are equal
module _ { l1 l2 : Level} (A : Metric-Space l1 l2) { f g : cauchy-approximation-Metric-Space A} ( f~g : map-cauchy-approximation-Metric-Space A f ~ map-cauchy-approximation-Metric-Space A g) where eq-htpy-cauchy-approximation-Metric-Space : f = g eq-htpy-cauchy-approximation-Metric-Space = eq-htpy-cauchy-approximation-Pseudometric-Space ( pseudometric-Metric-Space A) ( f~g)
References
Our definition of Cauchy approximation follows Definition 4.5.5 of [Boo20] and Definition 11.2.10 of [UF13].
- [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.
- [UF13]
- The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/, arXiv:1308.0729.
Recent changes
- 2025-08-18. malarbol and Louis Wasserman. Refactor metric spaces (#1450).
- 2025-05-27. malarbol. Zero approximations (#1424).
- 2025-05-01. malarbol. Limits of sequences in metric spaces (#1378).
- 2025-05-01. malarbol. The short map from a convergent Cauchy approximation in a saturated metric space to its limit (#1402).
- 2024-09-28. malarbol and Fredrik Bakke. Metric spaces (#1162).