Theorems · Theorem · sequences and series
Summable.tendsto_cofinite_zero
∀ {α : Type u_1} {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [IsTopologicalAddGroup G]
{f : α → G}, Summable f → Filter.Tendsto f Filter.cofinite (nhds 0)Series divergence test: if f is unconditionally summable, then f x tends to
zero along cofinite.
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 83 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.
- Setproof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Finsetproof · cited by 13,712
- AddCommGroupstatement and proof · cited by 12,871
- nhdsstatement and proof · cited by 5,554
- Finset.sumproof · cited by 5,195
- Filter.Tendstostatement · cited by 3,814
- Disjointproof · cited by 2,201
- SummationFilter.unconditionalstatement and proof · cited by 2,068
- IsTopologicalAddGroupstatement and proof · cited by 1,394
- Summablestatement and proof · cited by 778
- Filter.Eventually.monoproof · cited by 646
Cited by16
Results whose statement or proof uses this declaration.
- Summable.tendsto_atTop_zeroproof · cited by 10
- summable_geometric_iff_norm_lt_oneproof · cited by 4
- Summable.countable_supportproof · cited by 2
- Summable.hasFiniteSupport_of_discreteTopologyproof · cited by 2
- Complex.summable_log_one_add_of_summableproof · cited by 2
- Real.summable_log_one_add_of_summableproof · cited by 2
- IsUltrametricDist.norm_tsum_leproof · cited by 2
- NNReal.tendsto_cofinite_zero_of_summableproof · cited by 2
- Asymptotics.IsBigO.comp_summable_normproof · cited by 1
- Real.multipliable_one_add_of_summableproof · cited by 1
- Real.summable_nat_rpow_invproof · cited by 1
- summable_const_iffproof · cited by 1