Convergent series of real numbers

Content created by Louis Wasserman.

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

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

module real-numbers.convergent-series-real-numbers where
Imports 
open import analysis.convergent-series-metric-abelian-groups

open import foundation.propositions
open import foundation.universe-levels

open import real-numbers.dedekind-real-numbers
open import real-numbers.series-real-numbers

Idea

A series of real numbers converges to x if the sequence of its partial sums converges to x in the standard metric space of real numbers.

Definition

is-sum-prop-series-ℝ : {l : Level} → series-ℝ l → ℝ l → Prop l
is-sum-prop-series-ℝ = is-sum-prop-series-Metric-Ab

is-sum-series-ℝ : {l : Level} → series-ℝ l → ℝ l → UU l
is-sum-series-ℝ = is-sum-series-Metric-Ab

Recent changes