English
For natural numbers with a ≤ b, the product over Ico(a,b) extended by one at the top equals the product over Ico(a,b) times the top element: ∏_{k∈Ico(a,b+1)} f(k) = (∏_{k∈Ico(a,b)} f(k)) · f(b).
Русский
Для натуральных чисел a ≤ b произведение по Ico(a,b+1) равно произведению по Ico(a,b) на верхний элемент: ∏ f(k) по Ico(a,b+1) = (∏ f(k) по Ico(a,b)) · f(b).
LaTeX
$$$$ \\displaystyle \\prod_{k \\in \\mathrm{Ico}(a,b+1)} f(k) = \\left(\\prod_{k \\in \\mathrm{Ico}(a,b)} f(k)\\right) \\cdot f(b). $$$$
Lean4
@[to_additive]
theorem prod_Ico_succ_top {a b : ℕ} (hab : a ≤ b) (f : ℕ → M) :
(∏ k ∈ Ico a (b + 1), f k) = (∏ k ∈ Ico a b, f k) * f b := by
rw [← Finset.insert_Ico_right_eq_Ico_add_one hab, prod_insert right_notMem_Ico, mul_comm]
