The metric space of convergent sequences in metric spaces

Content created by malarbol.

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

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

open import metric-spaces.convergent-sequences-metric-spaces
open import metric-spaces.metric-spaces
open import metric-spaces.sequences-metric-spaces
open import metric-spaces.subspaces-metric-spaces

Idea

The convergent sequences in a metric space inherit the subbspace metric structure of the metric space of sequences. This defines the metric space of convergent sequences in a metric space.

Definitions

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

  metric-space-of-convergent-sequences-Metric-Space : Metric-Space (l1 ⊔ l2) l2
  metric-space-of-convergent-sequences-Metric-Space =
    subspace-Metric-Space
      ( sequence-Metric-Space M)
      ( subtype-convergent-sequence-Metric-Space M)

Recent changes