The action on convergent sequences of modulated uniformly continuous maps between metric spaces

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

module metric-spaces.action-on-convergent-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.convergent-sequences-metric-spaces
open import metric-spaces.limits-of-sequences-metric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.modulated-uniformly-continuous-maps-metric-spaces
open import metric-spaces.sequences-metric-spaces

Idea

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

Properties

Modulated uniformly continuous maps between metric spaces preserve convergent sequences and their limits

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 : convergent-sequence-Metric-Space A)
  where

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

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

  abstract
    is-limit-sequence-map-convergent-sequence-modulated-ucont-map-Metric-Space :
      is-limit-sequence-Metric-Space B
        ( sequence-map-convergent-sequence-modulated-ucont-map-Metric-Space)
        ( limit-sequence-map-convergent-sequence-modulated-ucont-map-Metric-Space)
    is-limit-sequence-map-convergent-sequence-modulated-ucont-map-Metric-Space =
      preserves-limits-sequence-modulated-ucont-map-Metric-Space
        ( A)
        ( B)
        ( f)
        ( seq-convergent-sequence-Metric-Space A u)
        ( limit-convergent-sequence-Metric-Space A u)
        ( is-limit-limit-convergent-sequence-Metric-Space A u)

  has-limit-sequence-map-convergent-sequence-modulated-ucont-map-Metric-Space :
    has-limit-sequence-Metric-Space B
      ( sequence-map-convergent-sequence-modulated-ucont-map-Metric-Space)
  has-limit-sequence-map-convergent-sequence-modulated-ucont-map-Metric-Space =
    ( limit-sequence-map-convergent-sequence-modulated-ucont-map-Metric-Space ,
      is-limit-sequence-map-convergent-sequence-modulated-ucont-map-Metric-Space)

  map-convergent-sequence-modulated-ucont-map-Metric-Space :
    convergent-sequence-Metric-Space B
  map-convergent-sequence-modulated-ucont-map-Metric-Space =
    ( sequence-map-convergent-sequence-modulated-ucont-map-Metric-Space ,
      has-limit-sequence-map-convergent-sequence-modulated-ucont-map-Metric-Space)

Recent changes