Theorems · Theorem · sequences and series

tendsto_tsum_compl_atTop_zero

∀ {α : Type u_1} {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [IsTopologicalAddGroup G]
  (f : α → G), Filter.Tendsto (fun s => ∑' (a : { x // x ∉ s }), f ↑a) Filter.atTop (nhds 0)

The sum over the complement of a finset tends to 0 when the finset grows to cover the whole space. This does not need a summability assumption, as otherwise all such sums are zero.

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Group

Cited by

3 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceAddCommGroupIsTopologicalAddGroup