prod_Ico_add — Mathlib

English

In the same setting, translating the other side of the index yields the same identity: ∏_{x∈Ico(a,b)} f(c+x) = ∏_{x∈Ico(a+c,b+c)} f(x).

Русский

В той же постановке, перенос по индексу слева даёт то же равенство: ∏_{x∈Ico(a,b)} f(c+x) = ∏_{x∈Ico(a+c,b+c)} f(x).

LaTeX

$$$$ \\displaystyle \\prod_{x \\in \\mathrm{Ico}(a,b)} f(c+x) = \\prod_{x \\in \\mathrm{Ico}(a+c,b+c)} f(x). $$$$

Lean4

@[to_additive]
theorem prod_Ico_add [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
    [LocallyFiniteOrder α] (f : α → M) (a b c : α) : (∏ x ∈ Ico a b, f (c + x)) = ∏ x ∈ Ico (a + c) (b + c), f x :=
  by
  convert prod_Ico_add' f a b c using 2
  rw [add_comm]

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