even_mul_odd — Mathlib

English

If f(n) has a convergent even-subsequence and a convergent odd-subsequence, then the whole sequence converges multiplicatively to the product of the two subsequential limits.

Русский

Если подпоследовательности чётных и нечётных индексов сходятся, то вся последовательность сходится к произведению двух пределов.

LaTeX

$$$\\text{HasProd}(f(2k))=m,\; \\text{HasProd}(f(2k+1))=m'\\Rightarrow \\text{HasProd}(f)=mm'$$$

Lean4

@[to_additive]
theorem even_mul_odd {f : ℕ → M} (he : Multipliable fun k ↦ f (2 * k)) (ho : Multipliable fun k ↦ f (2 * k + 1)) :
    Multipliable f :=
  (he.hasProd.even_mul_odd ho.hasProd).multipliable

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