Absolutely_Convergent_Series_is_Convergent

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

absolute-convergenceabsolutely-convergent-series-is-convergentbanach-spacesproofwiki

Let $V$ be a Banach space with norm $\norm {\, \cdot \,}$ . Let $\displaystyle \sum_{n \mathop = 1}^\infty a_n$ be an absolutely convergent series in $V$ . Then $\displaystyle \sum_{n \mathop = 1}^\infty a_n$ is convergent.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Topology.Algebra.InfiniteSum.Basic

Formal statement

import Mathlib.Analysis.Complex.Basic
import Mathlib.Topology.Algebra.InfiniteSum.Basic

theorem Absolutely_Convergent_Series_is_Convergent (a : ℕ → ℝ) (h : Summable (fun n => |a n|)) : Summable a := by sorry

Source

https://proofwiki.org/wiki/Absolutely_Convergent_Series_is_Convergent

View graph