Theorems · Theorem · sequences and series

tendsto_prod_nat_add

∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] (f : ℕ → G),
  Filter.Tendsto (fun i => ∏' (k : ℕ), f (k + i)) Filter.atTop (nhds 1)

For f : ℕ → G, the product ∏' k, f (k + i) tends to one. This does not require a multipliability assumption on f, as otherwise all such products are one.

Defined in

Mathlib.Topology.Algebra.InfiniteSum.NatInt

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommGroupTopologicalSpaceIsTopologicalGroupT2Space