The action on Cauchy sequences of short maps between metric spaces

Content created by Fredrik Bakke and Louis Wasserman.

Created on 2026-01-07.
Last modified on 2026-01-07.

module metric-spaces.action-on-cauchy-sequences-short-maps-metric-spaces where
Imports 
open import foundation.universe-levels

open import metric-spaces.action-on-cauchy-sequences-uniformly-continuous-maps-metric-spaces
open import metric-spaces.cauchy-sequences-metric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.short-maps-metric-spaces
open import metric-spaces.uniformly-continuous-maps-metric-spaces

Idea

The composition of a short map between metric spaces and a Cauchy sequence is a Cauchy sequence.

Proof

module _
  {l1 l2 l1' l2' : Level}
  (A : Metric-Space l1 l2) (B : Metric-Space l1' l2')
  (f : short-map-Metric-Space A B)
  (u : cauchy-sequence-Metric-Space A)
  where

  map-cauchy-sequence-short-map-Metric-Space :
    cauchy-sequence-Metric-Space B
  map-cauchy-sequence-short-map-Metric-Space =
    map-cauchy-sequence-uniformly-continuous-map-Metric-Space
      ( A)
      ( B)
      ( uniformly-continuous-map-short-map-Metric-Space A B f)
      ( u)

See also

Recent changes