prod_Ioo_mul_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 < b,\\ f:\\alpha\\to M,\\ (\\prod_{x\\in Ioo(a,b)} f(x))\\cdot f(a) = \\prod_{x\\in Ico(a,b)} f(x).$$$

Lean4

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

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