prod_eq_prod_Ico_succ_bot — Mathlib

English

For natural numbers a < b, the product over Ico a b equals f a times the product over Ico (a+1) b.

Русский

Для натуральных a < b произведение по Ico a b равно f(a) умноженному на произведение по Ico (a+1) b.

LaTeX

$$$\\forall a,b:\\mathbb{N},\\ hab:\\ a < b,\\ f:\\mathbb{N}\\to M,\\ \\prod_{k\\in Ico(a,b)} f(k) = f(a) \\cdot \\prod_{k\\in Ico(a+1,b)} f(k).$$$

Lean4

@[to_additive]
theorem prod_eq_prod_Ico_succ_bot {a b : ℕ} (hab : a < b) (f : ℕ → M) :
    ∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k :=
  by
  have ha : a ∉ Ico (a + 1) b := by simp
  rw [← prod_insert ha, Finset.insert_Ico_add_one_left_eq_Ico hab]

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