Sequences in premetric spaces

Content created by malarbol.

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

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

open import metric-spaces.premetric-spaces

Ideas

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

Definitions

Sequences in premetric spaces

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

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

Recent changes