The metric space of Lipschitz maps between metric spaces

Content created by Fredrik Bakke and Louis Wasserman.

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

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

open import metric-spaces.lipschitz-maps-metric-spaces
open import metric-spaces.metric-space-of-maps-metric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.subspaces-metric-spaces

Idea

Lipschitz maps between metric spaces inherit the metric subspace structure of the map metric space. This defines the metric space of Lipschitz maps between metric spaces.

Definitions

The metric space of Lipschitz maps between metric spaces

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

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

Recent changes