Sequences in metric spaces

Content created by Fredrik Bakke, Louis Wasserman and malarbol.

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

module metric-spaces.sequences-metric-spaces where

open import foundation.universe-levels

open import lists.sequences

open import metric-spaces.metric-spaces

Idea

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

Definition

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

  sequence-type-Metric-Space : UU l1
  sequence-type-Metric-Space = sequence (type-Metric-Space M)

Recent changes

• 2026-01-07. Louis Wasserman and Fredrik Bakke. Refactor Cauchy sequences (#1768).
• 2025-08-30. Louis Wasserman and Fredrik Bakke. Move sequences to lists namespace (#1476).
• 2025-05-01. malarbol. Limits of sequences in metric spaces (#1378).