Limits of Cauchy approximations in pseudometric spaces

Content created by Louis Wasserman and malarbol.

Created on 2025-08-18.
Last modified on 2025-08-18.

module metric-spaces.limits-of-cauchy-approximations-pseudometric-spaces where
Imports 
open import elementary-number-theory.positive-rational-numbers

open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import metric-spaces.cauchy-approximations-pseudometric-spaces
open import metric-spaces.pseudometric-spaces
open import metric-spaces.similarity-of-elements-pseudometric-spaces

Idea

A Cauchy approximation f : ℚ⁺ → A in a pseudometric space A has a limit x : A if f ε is near x for small ε : ℚ⁺; more precisely, if f ε is in a ε + δ-neighborhood of x for all ε δ : ℚ⁺.

Definitions

The property of having a limit in a pseudometric space

module _
  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
  (f : cauchy-approximation-Pseudometric-Space A)
  where

  is-limit-cauchy-approximation-prop-Pseudometric-Space :
    type-Pseudometric-Space A → Prop l2
  is-limit-cauchy-approximation-prop-Pseudometric-Space lim =
    Π-Prop
      ( ℚ⁺)
      ( λ ε →
        Π-Prop
          ( ℚ⁺)
          ( λ δ →
            neighborhood-prop-Pseudometric-Space
              ( A)
              ( ε +ℚ⁺ δ)
              ( map-cauchy-approximation-Pseudometric-Space A f ε)
              ( lim)))

  is-limit-cauchy-approximation-Pseudometric-Space :
    type-Pseudometric-Space A → UU l2
  is-limit-cauchy-approximation-Pseudometric-Space =
    type-Prop ∘ is-limit-cauchy-approximation-prop-Pseudometric-Space

Properties

Limits of a Cauchy approximations in a pseudometric space are similar

module _
  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
  (f : cauchy-approximation-Pseudometric-Space A)
  (x y : type-Pseudometric-Space A)
  where

  all-sim-is-limit-cauchy-approximation-Pseudometric-Space :
    is-limit-cauchy-approximation-Pseudometric-Space A f x →
    is-limit-cauchy-approximation-Pseudometric-Space A f y →
    sim-Pseudometric-Space A x y
  all-sim-is-limit-cauchy-approximation-Pseudometric-Space lim-x lim-y d =
    let
      (ε , δ , ε+δ=d) = split-ℚ⁺ d
      θ = mediant-zero-min-ℚ⁺ ε δ
      θ<ε = le-left-mediant-zero-min-ℚ⁺ ε δ
      θ<δ = le-right-mediant-zero-min-ℚ⁺ ε δ
      ε' = le-diff-ℚ⁺ θ ε θ<ε
      δ' = le-diff-ℚ⁺ θ δ θ<δ
      fθ = map-cauchy-approximation-Pseudometric-Space A f θ

      Nεx : neighborhood-Pseudometric-Space A ε fθ x
      Nεx =
        tr
          ( is-upper-bound-dist-Pseudometric-Space A fθ x)
          ( right-diff-law-add-ℚ⁺ θ ε θ<ε)
          ( lim-x θ ε')

      Nδy : neighborhood-Pseudometric-Space A δ fθ y
      Nδy =
        tr
          ( is-upper-bound-dist-Pseudometric-Space A fθ y)
          ( right-diff-law-add-ℚ⁺ θ δ θ<δ)
          ( lim-y θ δ')

      Nxy : neighborhood-Pseudometric-Space A (ε +ℚ⁺ δ) x y
      Nxy =
        triangular-neighborhood-Pseudometric-Space
          ( A)
          ( x)
          ( fθ)
          ( y)
          ( ε)
          ( δ)
          ( Nδy)
          ( symmetric-neighborhood-Pseudometric-Space A ε fθ x Nεx)
    in
      tr
        ( is-upper-bound-dist-Pseudometric-Space A x y)
        ( ε+δ=d)
        ( Nxy)

References

Our definition of limit of Cauchy approximation follows Definition 11.2.10 of [UF13].

[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