The metric space of isometries between metric spaces

Content created by Fredrik Bakke, Louis Wasserman and malarbol.

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

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

open import metric-spaces.isometries-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

Isometries between metric spaces inherit the metric subspace structure of the function metric space. This defines the metric space of isometries between metric spaces.

Definitions

The metric space of isometries between metric spaces

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

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

Recent changes