Cauchy sequences in metric spaces

Content created by Louis Wasserman, Fredrik Bakke and malarbol.

Created on 2025-03-23.
Last modified on 2026-01-07.

{-# OPTIONS --lossy-unification #-}

module metric-spaces.cauchy-sequences-metric-spaces where
Imports 
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.positive-rational-numbers

open import foundation.dependent-pair-types
open import foundation.functoriality-propositional-truncation
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import lists.sequences

open import metric-spaces.cartesian-products-metric-spaces
open import metric-spaces.cauchy-approximations-metric-spaces
open import metric-spaces.limits-of-sequences-metric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.modulated-cauchy-sequences-metric-spaces
open import metric-spaces.modulated-uniformly-continuous-maps-metric-spaces
open import metric-spaces.sequences-metric-spaces
open import metric-spaces.short-maps-metric-spaces

Idea

A Cauchy sequence x in a metric space X is a sequence of elements of X such that there exists a modulus making it a modulated Cauchy sequence.

Definition

Cauchy sequences

module _
  {l1 l2 : Level}
  (X : Metric-Space l1 l2)
  (x : sequence-type-Metric-Space X)
  where

  is-cauchy-sequence-prop-Metric-Space : Prop l2
  is-cauchy-sequence-prop-Metric-Space =
    trunc-Prop (cauchy-modulus-sequence-Metric-Space X x)

  is-cauchy-sequence-Metric-Space : UU l2
  is-cauchy-sequence-Metric-Space =
    type-Prop is-cauchy-sequence-prop-Metric-Space

cauchy-sequence-Metric-Space :
  {l1 l2 : Level} → Metric-Space l1 l2 → UU (l1 ⊔ l2)
cauchy-sequence-Metric-Space X =
  type-subtype (is-cauchy-sequence-prop-Metric-Space X)

cauchy-sequence-modulated-cauchy-sequence-Metric-Space :
  {l1 l2 : Level} (M : Metric-Space l1 l2) →
  modulated-cauchy-sequence-Metric-Space M →
  cauchy-sequence-Metric-Space M
cauchy-sequence-modulated-cauchy-sequence-Metric-Space
  M (x , μx) = (x , unit-trunc-Prop μx)

module _
  {l1 l2 : Level}
  (X : Metric-Space l1 l2)
  (x : cauchy-sequence-Metric-Space X)
  where

  sequence-cauchy-sequence-Metric-Space : sequence-type-Metric-Space X
  sequence-cauchy-sequence-Metric-Space = pr1 x

  is-cauchy-sequence-sequence-cauchy-sequence-Metric-Space :
    is-cauchy-sequence-Metric-Space X sequence-cauchy-sequence-Metric-Space
  is-cauchy-sequence-sequence-cauchy-sequence-Metric-Space = pr2 x

Properties

A sequence with a limit is Cauchy

module _
  {l1 l2 : Level}
  (X : Metric-Space l1 l2)
  {x : sequence-type-Metric-Space X}
  where

  abstract
    is-cauchy-has-limit-sequence-Metric-Space :
      has-limit-sequence-Metric-Space X x → is-cauchy-sequence-Metric-Space X x
    is-cauchy-has-limit-sequence-Metric-Space (lim , is-lim-x) =
      map-trunc-Prop
        ( cauchy-modulus-limit-modulus-sequence-Metric-Space X x lim)
        ( is-lim-x)

Pairing of Cauchy sequences

module _
  {l1 l2 l3 l4 : Level}
  (A : Metric-Space l1 l2) (B : Metric-Space l3 l4)
  (u : cauchy-sequence-Metric-Space A)
  (v : cauchy-sequence-Metric-Space B)
  where

  sequence-pair-cauchy-sequence-Metric-Space :
    sequence-type-Metric-Space (product-Metric-Space A B)
  sequence-pair-cauchy-sequence-Metric-Space =
    pair-sequence
      ( sequence-cauchy-sequence-Metric-Space A u)
      ( sequence-cauchy-sequence-Metric-Space B v)

  abstract
    is-cauchy-sequence-pair-cauchy-sequence-Metric-Space :
      is-cauchy-sequence-Metric-Space
        ( product-Metric-Space A B)
        ( sequence-pair-cauchy-sequence-Metric-Space)
    is-cauchy-sequence-pair-cauchy-sequence-Metric-Space =
      let
        open
          do-syntax-trunc-Prop
            ( is-cauchy-sequence-prop-Metric-Space
              ( product-Metric-Space A B)
              ( sequence-pair-cauchy-sequence-Metric-Space))
      in do
        μ-u ← is-cauchy-sequence-sequence-cauchy-sequence-Metric-Space A u
        μ-v ← is-cauchy-sequence-sequence-cauchy-sequence-Metric-Space B v
        unit-trunc-Prop
          ( is-cauchy-seq-pair-modulated-cauchy-sequence-Metric-Space
            ( A)
            ( B)
            ( sequence-cauchy-sequence-Metric-Space A u , μ-u)
            ( sequence-cauchy-sequence-Metric-Space B v , μ-v))

  pair-cauchy-sequence-Metric-Space :
    cauchy-sequence-Metric-Space (product-Metric-Space A B)
  pair-cauchy-sequence-Metric-Space =
    ( sequence-pair-cauchy-sequence-Metric-Space ,
      is-cauchy-sequence-pair-cauchy-sequence-Metric-Space)

To show a sequence a is Cauchy, it suffices to exhibit a modulus function μ such that for any ε, a (μ ε) and a (μ ε + k) are in an ε-neighborhood

module
  _
  {l1 l2 : Level}
  (X : Metric-Space l1 l2)
  (a : sequence-type-Metric-Space X)
  (μ : ℚ⁺ → ℕ)
  where

  abstract
    is-cauchy-sequence-modulus-neighborhood-add-sequence-Metric-Space :
      ( (ε : ℚ⁺) (k : ℕ) →
        neighborhood-Metric-Space X ε (a (μ ε)) (a (μ ε +ℕ k))) →
      is-cauchy-sequence-Metric-Space X a
    is-cauchy-sequence-modulus-neighborhood-add-sequence-Metric-Space H =
      unit-trunc-Prop
        ( cauchy-modulus-neighborhood-add-sequence-Metric-Space X a μ H)

See also

Recent changes