The metric abelian group of real numbers

Content created by Louis Wasserman.

Created on 2025-12-03.
Last modified on 2025-12-03.

{-# OPTIONS --lossy-unification #-}

module real-numbers.metric-additive-group-of-real-numbers where
Imports 
open import analysis.complete-metric-abelian-groups
open import analysis.metric-abelian-groups

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

open import metric-spaces.pseudometric-spaces

open import real-numbers.cauchy-completeness-dedekind-real-numbers
open import real-numbers.isometry-addition-real-numbers
open import real-numbers.isometry-negation-real-numbers
open import real-numbers.large-additive-group-of-real-numbers
open import real-numbers.metric-space-of-real-numbers

Idea

The Dedekind real numbers form a metric abelian group under addition with regards to their standard metric space.

Definition

metric-ab-add-ℝ : (l : Level) → Metric-Ab (lsuc l) l
metric-ab-add-ℝ l =
  ( ab-add-ℝ l ,
    structure-Pseudometric-Space (pseudometric-space-ℝ l) ,
    is-extensional-pseudometric-space-ℝ ,
    is-isometry-neg-ℝ ,
    is-isometry-left-add-ℝ)

complete-metric-ab-add-ℝ : (l : Level) → Complete-Metric-Ab (lsuc l) l
complete-metric-ab-add-ℝ l =
  ( metric-ab-add-ℝ l ,
    is-complete-metric-space-ℝ l)

Recent changes