of_add_one_of_neg_add_one — Mathlib

English

If the positive and negative halves converge multiplicably, then the whole function is multiplicable: Multipliable f.

Русский

Если обе половины произведения сходятся, тогда полное двустороннее произведение сходится: Multipliable f.

LaTeX

$$$\\displaystyle \\bigl( \\text{Multipliable} \\ f \\bigr) \\,=\, \\bigl( \\text{Multipliable} \\bigl( n \\mapsto f(n) \\bigr) \\land \\text{Multipliable} \\bigl( n \\mapsto f(-n) \\bigr) \\bigr)$$$

Lean4

@[to_additive Summable.of_add_one_of_neg_add_one]
theorem of_add_one_of_neg_add_one {f : ℤ → M} (hf₁ : Multipliable fun n : ℕ ↦ f (n + 1))
    (hf₂ : Multipliable fun n : ℕ ↦ f (-(n + 1))) : Multipliable f :=
  (hf₁.hasProd.of_add_one_of_neg_add_one hf₂.hasProd).multipliable

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