tprod_pnat_eq_tprod_succ — Mathlib

English

The bilateral tprod over positive naturals satisfies ∏' n:ℕ+, f n = ∏' n, f (n+1).

Русский

Двоичное т-произведение по положительным натуральным числам равно произведению по всем натуральным числам сдвинутым на 1.

LaTeX

$$$\\displaystyle \\prod'_{n:\\mathbb{N}^+} f(n) = \\prod'_{n\\in\\mathbb{N}} f(n+1)$$$

Lean4

@[to_additive]
theorem tprod_pnat_eq_tprod_succ {f : ℕ → M} : ∏' n : ℕ+, f n = ∏' n, f (n + 1) :=
  (Equiv.pnatEquivNat.symm.tprod_eq _).symm

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