Sequences in metric spaces

Content created by malarbol.

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

module metric-spaces.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

A sequence in a metric space is a sequence in its underlying type.

Definitions

The metric space of sequences in a metric space

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

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

  sequence-type-Metric-Space : UU l1
  sequence-type-Metric-Space =
    type-Metric-Space sequence-Metric-Space

Recent changes