The metric space of uniformly continuous maps between metric spaces

Content created by Louis Wasserman.

Created on 2026-03-03.
Last modified on 2026-03-03.

module metric-spaces.metric-space-of-uniformly-continuous-maps-metric-spaces where
Imports 
open import foundation.universe-levels

open import metric-spaces.metric-space-of-maps-metric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.subspaces-metric-spaces
open import metric-spaces.uniformly-continuous-maps-metric-spaces

Idea

Uniformly continuous maps between metric spaces inherit the metric subspace structure of the function metric space. This defines the metric space of uniformly continuous maps between metric spaces.

Definitions

The metric space of uniformly continuous maps between metric spaces

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

  metric-space-of-uniformly-continuous-maps-Metric-Space :
    Metric-Space (l1 ⊔ l2 ⊔ l1' ⊔ l2') (l1 ⊔ l2')
  metric-space-of-uniformly-continuous-maps-Metric-Space =
    subspace-Metric-Space
      ( metric-space-of-maps-Metric-Space A B)
      ( is-uniformly-continuous-prop-map-Metric-Space A B)

Recent changes