Modulated Cauchy sequences in the real numbers

Content created by Fredrik Bakke and Louis Wasserman.

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

module real-numbers.modulated-cauchy-sequences-real-numbers where
Imports 
open import foundation.universe-levels

open import lists.sequences

open import metric-spaces.modulated-cauchy-sequences-metric-spaces

open import real-numbers.dedekind-real-numbers
open import real-numbers.metric-space-of-real-numbers

Idea

A modulated Cauchy sequence in the real numbers is a modulated Cauchy sequence in the metric space of real numbers

Definition

cauchy-modulus-sequence-ℝ : {l : Level} → sequence (ℝ l) → UU l
cauchy-modulus-sequence-ℝ {l} =
  cauchy-modulus-sequence-Metric-Space (metric-space-ℝ l)

modulated-cauchy-sequence-ℝ : (l : Level) → UU (lsuc l)
modulated-cauchy-sequence-ℝ l =
  modulated-cauchy-sequence-Metric-Space (metric-space-ℝ l)

Recent changes