The metric space of short functions between metric spaces

Content created by malarbol.

Created on 2025-05-05.
Last modified on 2025-05-05.

module metric-spaces.metric-space-of-short-functions-metric-spaces where
Imports 
open import foundation.universe-levels

open import metric-spaces.metric-space-of-functions-metric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.short-functions-metric-spaces
open import metric-spaces.subspaces-metric-spaces

Idea

Short functions between metric spaces inherit the metric subspace structure of the function metric space. This defines the metric space of short functions between metric spaces.

Definitions

The metric space of short functions between metric spaces

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

  metric-space-of-short-functions-Metric-Space :
    Metric-Space (l1 ⊔ l2 ⊔ l1' ⊔ l2') (l1 ⊔ l2')
  metric-space-of-short-functions-Metric-Space =
    subspace-Metric-Space
      ( metric-space-of-functions-Metric-Space A B)
      ( is-short-function-prop-Metric-Space A B)

Recent changes