Sequences in pseudometric spaces

Content created by malarbol.

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

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

open import metric-spaces.pseudometric-spaces
open import metric-spaces.sequences-premetric-spaces

Ideas

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

Definition

Sequences in pseudometric spaces

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

  sequence-type-Pseudometric-Space : UU l1
  sequence-type-Pseudometric-Space =
    sequence-type-Premetric-Space (premetric-Pseudometric-Space M)

Recent changes