Images of metric spaces

Content created by Louis Wasserman.

Created on 2025-08-31.
Last modified on 2025-08-31.

module metric-spaces.images-metric-spaces where
Imports 
open import foundation.images
open import foundation.universe-levels

open import metric-spaces.functions-metric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.subspaces-metric-spaces

Idea

Given a function between metric spaces f : X → Y, the image of X under f is a subspace of Y.

Definition

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

  im-Metric-Space : Metric-Space (l1 ⊔ l3) l4
  im-Metric-Space = subspace-Metric-Space Y (subtype-im f)

Recent changes