mul_prod_Ioo_eq_prod_Ico — Mathlib

English

For a ≤ b, the product over Ioo a b times f(a) equals the product over Ico a b.

Русский

Для a ≤ b произведение по Ioo a b умноженное на f(a) равно произведению по Ico a b.

LaTeX

$$$\\text{If } a \\le b,\\ f:\\alpha\\to M,\\ f(a)\\cdot \\prod_{x\\in Ioo(a,b)} f(x) = \\prod_{x\\in Ico(a,b)} f(x).$$$

Lean4

@[to_additive]
theorem mul_prod_Ioo_eq_prod_Ico (h : a < b) : f a * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ico a b, f x := by
  rw [Ico_eq_cons_Ioo h, prod_cons]

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