Theorems · Theorem · sequences and series
summable_iff_nat_tsum_vanishing
∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G] [CompleteSpace G] {f : ℕ → G},
Summable f ↔ ∀ e ∈ nhds 0, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ e- Cited by
- 1 results in Mathlib
- Foundations
- Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- AddCommGroupstatement and proof · cited by 12,871
- Filterstatement · cited by 8,121
- Set.Elemstatement and proof · cited by 7,166
- Set.ofPredstatement and proof · cited by 6,101
- nhdsstatement and proof · cited by 5,554
- CompleteSpacestatement and proof · cited by 2,532
- SummationFilter.unconditionalstatement and proof · cited by 2,068
- UniformSpacestatement and proof · cited by 2,040
- tsumstatement and proof · cited by 1,148
- Summablestatement · cited by 778
- IsUniformAddGroupstatement and proof · cited by 342
Cited by1
Results whose statement or proof uses this declaration.
- EulerProduct.norm_tsum_factoredNumbers_sub_tsum_ltproof · cited by 2