prod_Ico_mul_eq_prod_Icc — Mathlib

English

For a ≤ b in a LocallyFiniteOrdered set, the product over Ico a b of f equals the product over Icc a b divided by f b, equivalently

Русский

При a ≤ b в локально конечном упорядоченном множестве произведение по Ico a b равно произведению по Icc a b поделённому на f(b).

LaTeX

$$$\\Any (a,b):\\alpha,\\ a\\le b \\Rightarrow (\\prod_{x\\in Ico(a,b)} f(x)) = (\\prod_{x\\in Icc(a,b)} f(x)) / f(b).$$$

Lean4

@[to_additive]
theorem prod_Ico_mul_eq_prod_Icc (h : a ≤ b) : (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Icc a b, f x := by
  rw [mul_comm, mul_prod_Ico_eq_prod_Icc h]

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