prod_Ioo_mul_eq_prod_Ioc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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