prod_Ico_mul_eq_prod_Ico_add_one — Mathlib

English

Let a ≤ b in a linear order with LocallyFiniteOrder, and f: α → M. Then (∏_{x ∈ Ico(a,b)} f(x)) · f(b) = ∏_{x ∈ Ico(a,b+1)} f(x).

Русский

Пусть a ≤ b в линейном порядке и f: α → M. Тогда (∏_{x ∈ Ico(a,b)} f(x)) · f(b) = ∏_{x ∈ Ico(a,b+1)} f(x).

LaTeX

$$$ \left(\prod_{x \in \mathrm{Ico}(a,b)} f(x)\right) \cdot f(b) = \prod_{x \in \mathrm{Ico}(a,(b+1))} f(x) $$$

Lean4

theorem prod_Ico_mul_eq_prod_Ico_add_one (hab : a ≤ b) (f : α → M) :
    (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Ico a (b + 1), f x := by
  rw [← Finset.insert_Ico_right_eq_Ico_add_one hab, prod_insert right_notMem_Ico, mul_comm]

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