comp_nat_add — Mathlib

English

For a multiplicative function f on a countable index, having a product limit m is equivalent to the partial products tending to m.

Русский

Для умножаемой функции f на исчисляемом индексе равенство предела произведения m эквивалентно переходу частичных произведений к m.

LaTeX

$$$\\text{HasProd}(f,m) \\iff \\operatorname{Tendsto}(n \\mapsto \\prod_{i=0}^{n-1} f(i))\\;\\text{atTop}\\; (\\mathcal{nhds}\\, m)$$$

Lean4

@[to_additive]
theorem comp_nat_add {f : ℕ → M} {k : ℕ} (h : Multipliable fun n ↦ f (n + k)) : Multipliable f :=
  h.hasProd.prod_range_mul.multipliable

Похожие утверждения