The action on modulated Cauchy sequences of modulated uniformly continuous 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-modulated-cauchy-sequences-modulated-uniformly-continuous-maps-metric-spaces where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import lists.sequences

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

The composition of a modulated uniformly continuous map between metric spaces and a modulated Cauchy sequence is a modulated Cauchy sequence.

Properties

Modulated uniformly continuous maps between metric spaces preserve modulated Cauchy sequences

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

  sequence-map-modulated-cauchy-sequence-modulated-ucont-map-Metric-Space :
    sequence-type-Metric-Space B
  sequence-map-modulated-cauchy-sequence-modulated-ucont-map-Metric-Space =
    map-sequence
      ( map-modulated-ucont-map-Metric-Space A B f)
      ( sequence-modulated-cauchy-sequence-Metric-Space A u)

  abstract
    cauchy-modulus-map-modulated-cauchy-sequence-modulated-ucont-map-Metric-Space :
      cauchy-modulus-sequence-Metric-Space B
        ( sequence-map-modulated-cauchy-sequence-modulated-ucont-map-Metric-Space)
    cauchy-modulus-map-modulated-cauchy-sequence-modulated-ucont-map-Metric-Space
      ε =
      let
        (map-f , μf , is-mod-μf) = f
        (seq-u , μu) = u
        (N , H) = μu (μf ε)
      in
        ( N ,
          λ n k N≤n N≤k → is-mod-μf (seq-u n) ε (seq-u k) (H n k N≤n N≤k))

  map-modulated-cauchy-sequence-modulated-ucont-map-Metric-Space :
    modulated-cauchy-sequence-Metric-Space B
  map-modulated-cauchy-sequence-modulated-ucont-map-Metric-Space =
    ( sequence-map-modulated-cauchy-sequence-modulated-ucont-map-Metric-Space ,
      cauchy-modulus-map-modulated-cauchy-sequence-modulated-ucont-map-Metric-Space)

Recent changes