Sequences in metric abelian groups

Content created by Louis Wasserman.

Created on 2026-01-11.
Last modified on 2026-01-11.

module analysis.sequences-metric-abelian-groups where
Imports 
open import analysis.metric-abelian-groups

open import foundation.universe-levels

open import lists.sequences

Idea

A sequence in a metric abelian group inherits the operations of the group.

Definition

sequence-type-Metric-Ab : {l1 l2 : Level} → Metric-Ab l1 l2 → UU l1
sequence-type-Metric-Ab G = sequence (type-Metric-Ab G)

add-sequence-type-Metric-Ab :
  {l1 l2 : Level} (G : Metric-Ab l1 l2) →
  sequence-type-Metric-Ab G → sequence-type-Metric-Ab G →
  sequence-type-Metric-Ab G
add-sequence-type-Metric-Ab G = binary-map-sequence (add-Metric-Ab G)

neg-sequence-type-Metric-Ab :
  {l1 l2 : Level} (G : Metric-Ab l1 l2) →
  sequence-type-Metric-Ab G → sequence-type-Metric-Ab G
neg-sequence-type-Metric-Ab G = map-sequence (neg-Metric-Ab G)

Recent changes