The metric space of sequences in a metric space

Content created by Fredrik Bakke and Louis Wasserman.

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

module metric-spaces.metric-space-of-sequences-metric-spaces where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.universe-levels

open import metric-spaces.dependent-products-metric-spaces
open import metric-spaces.metric-spaces

Idea

The type of sequences in a metric space itself forms a metric space.

Definition

module _
  {l1 l2 : Level} (M : Metric-Space l1 l2)
  where

  sequence-Metric-Space : Metric-Space l1 l2
  sequence-Metric-Space = Π-Metric-Space ℕ (λ _ → M)

Recent changes