prod_Icc_succ_top — Mathlib

English

For Icc intervals, extending the upper endpoint multiplies by the new top value: ∏_{k∈Icc(a,b+1)} f(k) = (∏_{k∈Icc(a,b)} f(k)) · f(b+1).

Русский

Для интервалов Icc(a,b+1) произведение равно произведению по Icc(a,b) умноженному на f(b+1).

LaTeX

$$$$ \\displaystyle \\prod_{k \\in \\mathrm{Icc}(a,b+1)} f(k) = \\left(\\prod_{k \\in \\mathrm{Icc}(a,b)} f(k)\\right) \\cdot f(b+1). $$$$

Lean4

@[to_additive]
theorem prod_Icc_succ_top {a b : ℕ} (hab : a ≤ b + 1) (f : ℕ → M) :
    (∏ k ∈ Icc a (b + 1), f k) = (∏ k ∈ Icc a b, f k) * f (b + 1) := by
  rw [← Ico_add_one_right_eq_Icc, prod_Ico_succ_top hab, Ico_add_one_right_eq_Icc]

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