Uniformly continuous functions between metric spaces

Content created by Louis Wasserman and malarbol.

Created on 2025-03-30.
Last modified on 2025-10-19.

module metric-spaces.uniformly-continuous-functions-metric-spaces where

open import elementary-number-theory.positive-rational-numbers

open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.inhabited-subtypes
open import foundation.inhabited-types
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import logic.functoriality-existential-quantification

open import metric-spaces.continuous-functions-metric-spaces
open import metric-spaces.functions-metric-spaces
open import metric-spaces.isometries-metric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.modulated-uniformly-continuous-functions-metric-spaces
open import metric-spaces.sequences-metric-spaces
open import metric-spaces.short-functions-metric-spaces

Idea

A function f between metric spaces X and Y is uniformly continuous^¶ if there exists a modulus of uniform continuity for it.

Definitions

The property of being a uniformly continuous function

module _
  {l1 l2 l3 l4 : Level}
  (X : Metric-Space l1 l2)
  (Y : Metric-Space l3 l4)
  (f : type-function-Metric-Space X Y)
  where

  is-uniformly-continuous-prop-function-Metric-Space : Prop (l1 ⊔ l2 ⊔ l4)
  is-uniformly-continuous-prop-function-Metric-Space =
    is-inhabited-Prop
      (modulus-of-uniform-continuity-function-Metric-Space X Y f)

  is-uniformly-continuous-function-Metric-Space : UU (l1 ⊔ l2 ⊔ l4)
  is-uniformly-continuous-function-Metric-Space =
    type-Prop is-uniformly-continuous-prop-function-Metric-Space

The type of uniformly continuous functions between metric spaces

module _
  {l1 l2 l3 l4 : Level} (X : Metric-Space l1 l2) (Y : Metric-Space l3 l4)
  where

  uniformly-continuous-function-Metric-Space : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  uniformly-continuous-function-Metric-Space =
    type-subtype (is-uniformly-continuous-prop-function-Metric-Space X Y)

  map-uniformly-continuous-function-Metric-Space :
    uniformly-continuous-function-Metric-Space →
    type-function-Metric-Space X Y
  map-uniformly-continuous-function-Metric-Space = pr1

  is-uniformly-continuous-map-uniformly-continuous-function-Metric-Space :
    (f : uniformly-continuous-function-Metric-Space) →
    is-uniformly-continuous-function-Metric-Space
      ( X)
      ( Y)
      ( map-uniformly-continuous-function-Metric-Space f)
  is-uniformly-continuous-map-uniformly-continuous-function-Metric-Space =
    pr2

  uniformly-continuous-function-modulated-ucont-map-Metric-Space :
    modulated-ucont-map-Metric-Space X Y →
    uniformly-continuous-function-Metric-Space
  uniformly-continuous-function-modulated-ucont-map-Metric-Space (f , m) =
    (f , unit-trunc-Prop m)

Properties

Uniformly continuous functions are continuous everywhere

module _
  {l1 l2 l3 l4 : Level}
  (X : Metric-Space l1 l2)
  (Y : Metric-Space l3 l4)
  (f : type-function-Metric-Space X Y)
  where

  is-continuous-at-point-is-uniformly-continuous-function-Metric-Space :
    is-uniformly-continuous-function-Metric-Space X Y f →
    (x : type-Metric-Space X) →
    is-continuous-at-point-function-Metric-Space X Y f x
  is-continuous-at-point-is-uniformly-continuous-function-Metric-Space H x =
    rec-trunc-Prop
      ( is-continuous-at-point-prop-function-Metric-Space X Y f x)
      ( λ m →
        is-continuous-at-point-map-modulated-ucont-map-Metric-Space X Y
          ( f , m)
          ( x))
      ( H)

The identity function is uniformly continuous

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

  is-uniformly-continuous-id-Metric-Space :
    is-uniformly-continuous-function-Metric-Space X X id
  is-uniformly-continuous-id-Metric-Space =
    intro-exists id (λ _ _ _ → id)

The composition of uniformly continuous functions is uniformly continuous

module _
  {l1 l2 l3 l4 l5 l6 : Level}
  (X : Metric-Space l1 l2)
  (Y : Metric-Space l3 l4)
  (Z : Metric-Space l5 l6)
  where

  is-uniformly-continuous-comp-function-Metric-Space :
    (g : type-function-Metric-Space Y Z) →
    (f : type-function-Metric-Space X Y) →
    is-uniformly-continuous-function-Metric-Space Y Z g →
    is-uniformly-continuous-function-Metric-Space X Y f →
    is-uniformly-continuous-function-Metric-Space X Z (g ∘ f)
  is-uniformly-continuous-comp-function-Metric-Space g f H K =
    let
      open
        do-syntax-trunc-Prop
          ( is-uniformly-continuous-prop-function-Metric-Space X Z (g ∘ f))
    in
      do
        mg , is-modulus-uniform-mg ← H
        mf , is-modulus-uniform-mf ← K
        intro-exists
          ( mf ∘ mg)
          ( λ x ε x' →
            is-modulus-uniform-mg (f x) ε (f x') ∘
            is-modulus-uniform-mf x (mg ε) x')

  comp-uniformly-continuous-function-Metric-Space :
    uniformly-continuous-function-Metric-Space Y Z →
    uniformly-continuous-function-Metric-Space X Y →
    uniformly-continuous-function-Metric-Space X Z
  comp-uniformly-continuous-function-Metric-Space g f =
    ( map-uniformly-continuous-function-Metric-Space Y Z g ∘
      map-uniformly-continuous-function-Metric-Space X Y f) ,
    ( is-uniformly-continuous-comp-function-Metric-Space
      ( map-uniformly-continuous-function-Metric-Space Y Z g)
      ( map-uniformly-continuous-function-Metric-Space X Y f)
      ( is-uniformly-continuous-map-uniformly-continuous-function-Metric-Space
        ( Y)
        ( Z)
        ( g))
      ( is-uniformly-continuous-map-uniformly-continuous-function-Metric-Space
        ( X)
        ( Y)
        ( f)))

Short maps are uniformly continuous

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

  is-uniformly-continuous-is-short-function-Metric-Space :
    (f : type-function-Metric-Space A B) →
    is-short-function-Metric-Space A B f →
    is-uniformly-continuous-function-Metric-Space A B f
  is-uniformly-continuous-is-short-function-Metric-Space f H =
    intro-exists id (λ x d → H d x)

  uniformly-continuous-short-function-Metric-Space :
    short-function-Metric-Space A B →
    uniformly-continuous-function-Metric-Space A B
  uniformly-continuous-short-function-Metric-Space =
    tot is-uniformly-continuous-is-short-function-Metric-Space

Isometries are uniformly continuous

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

  is-uniformly-continuous-is-isometry-Metric-Space :
    (f : type-function-Metric-Space A B) →
    is-isometry-Metric-Space A B f →
    is-uniformly-continuous-function-Metric-Space A B f
  is-uniformly-continuous-is-isometry-Metric-Space f =
    is-uniformly-continuous-is-short-function-Metric-Space A B f ∘
    is-short-is-isometry-Metric-Space A B f

  uniformly-continuous-isometry-Metric-Space :
    isometry-Metric-Space A B →
    uniformly-continuous-function-Metric-Space A B
  uniformly-continuous-isometry-Metric-Space =
    tot is-uniformly-continuous-is-isometry-Metric-Space

See also

• Modulated uniformly continuous functions on metric spaces

External links

• Uniform continuity at Wikidata

Recent changes

• 2025-10-19. Louis Wasserman. Adding limits and Cauchy sequences in the real numbers (#1603).
• 2025-08-31. Louis Wasserman. The image of a totally bounded metric space under a uniformly continuous function is totally bounded (#1513).
• 2025-08-18. malarbol and Louis Wasserman. Refactor metric spaces (#1450).
• 2025-05-19. malarbol. Lipschitz-continuous functions between metric spaces (#1417).
• 2025-03-30. Louis Wasserman. Continuity of functions between metric spaces (#1375).