The metric additive group of rational numbers

Content created by Louis Wasserman.

Created on 2025-11-06.
Last modified on 2025-11-06.

module elementary-number-theory.metric-additive-group-of-rational-numbers where
Imports 
open import analysis.metric-abelian-groups

open import elementary-number-theory.addition-rational-numbers
open import elementary-number-theory.additive-group-of-rational-numbers
open import elementary-number-theory.rational-numbers

open import foundation.dependent-pair-types
open import foundation.universe-levels

open import metric-spaces.metric-space-of-rational-numbers
open import metric-spaces.metric-spaces

Idea

Addition on the rational numbers forms a metric abelian group.

Definition

metric-ab-add-ℚ : Metric-Ab lzero lzero
metric-ab-add-ℚ =
  ( abelian-group-add-ℚ ,
    pseudometric-structure-Metric-Space metric-space-ℚ ,
    is-extensional-pseudometric-space-ℚ ,
    is-isometry-neg-ℚ ,
    is-isometry-add-ℚ)

Recent changes