Theorems · Theorem · sequences and series
Summable.tendsto_sum_tsum_nat
∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {f : ℕ → M},
Summable f → Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds (∑' (i : ℕ), f i))If f : ℕ → M is summable, then the partial sums ∑ i ∈ range n, f i converge
to ∑' i, f i.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- AddCommMonoidstatement and proof · cited by 12,281
- nhdsstatement · cited by 5,554
- Finset.sumstatement · cited by 5,195
- Filter.Tendstostatement · cited by 3,814
- Filter.atTopstatement · cited by 2,405
- SummationFilter.unconditionalstatement and proof · cited by 2,068
- Finset.rangestatement · cited by 1,341
- tsumstatement · cited by 1,148
- Summablestatement and proof · cited by 778
- Summable.hasSumproof · cited by 184
- HasSum.tendsto_sum_natproof · cited by 23
Cited by3
Results whose statement or proof uses this declaration.
- isCompact_setOfPred_finiteMeasure_mass_le_compl_isCompact_leproof · cited by 2
- AntitoneOn.integral_le_tsum_comp_addproof · cited by 1
- Summable.tendsto_alternating_series_tsumproof · cited by 1