Theorems · Theorem · functional analysis

NormedAddCommGroup.completeSpace_of_summable_imp_tendsto

∀ {E : Type u_1} [inst : NormedAddCommGroup E],
  (∀ (u : ℕ → E),
      (Summable fun x => ‖u x‖) → ∃ a, Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, u i) Filter.atTop (nhds a)) →
    CompleteSpace E

A normed additive group is complete if any absolutely convergent series converges in the space.

Defined in: Mathlib.Analysis.Normed.Group.Completeness
Cited by: 1 results in Mathlib
Foundations: Depth 163 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites22

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement · cited by 25,697
NormedAddCommGroupstatement and proof · cited by 15,752
nhdsstatement and proof · cited by 5,554
Norm.normstatement and proof · cited by 5,413
Finset.sumstatement and proof · cited by 5,195
Filter.Tendstostatement and proof · cited by 3,814
CompleteSpacestatement · cited by 2,532
Filter.atTopstatement and proof · cited by 2,405
SummationFilter.unconditionalstatement and proof · cited by 2,068
Dist.distproof · cited by 1,539
Finset.rangestatement and proof · cited by 1,341
Summablestatement and proof · cited by 778

Cited by1

Results whose statement or proof uses this declaration.

NormedAddCommGroup.summable_imp_tendsto_iff_completeSpaceproof · cited by 0