mul_prod_Ioc_eq_prod_Icc — Mathlib

English

For a ≤ b, multiply the product over Ioo a b by f(a) to obtain the product over Icc a b.

Русский

При a ≤ b умножение произведения по Ioo a b на f(a) даёт произведение по Icc 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 Icc(a,b)} f(x).$$$

Lean4

@[to_additive]
theorem mul_prod_Ioc_eq_prod_Icc (h : a ≤ b) : f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x := by
  rw [Icc_eq_cons_Ioc h, prod_cons]

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