mul_prod_Ioo_eq_prod_Ioc — Mathlib

English

For a < b, the product over Ioo a b times f(a) equals the product over Ioc a b.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mul_prod_Ioo_eq_prod_Ioc (h : a < b) : f b * ∏ x ∈ Ioo a b, f x = ∏ x ∈ Ioc a b, f x := by
  rw [Ioc_eq_cons_Ioo h, prod_cons]

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