Theorems · Theorem · functional analysis
NormedAddCommGroup.summable_imp_tendsto_of_complete
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [CompleteSpace E] (u : ℕ → E),
(Summable fun x => ‖u x‖) → ∃ a, Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, u i) Filter.atTop (nhds a)In a complete normed additive group, every absolutely convergent series converges in the space.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
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 · cited by 5,554
- Norm.normstatement and proof · cited by 5,413
- Finset.sumstatement and proof · cited by 5,195
- Filter.Tendstostatement · cited by 3,814
- CompleteSpacestatement and proof · cited by 2,532
- Filter.atTopstatement · 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