English
If subtraction is defined, shifting the interval by c and subtracting c recovers the original product: ∏_{x∈Ico(a+c,b+c)} f(x−c) = ∏_{x∈Ico(a,b)} f(x).
Русский
При наличии операции вычитания: перенос интервала на c и вычитание c восстанавливают исходное произведение: ∏_{x∈Ico(a+c,b+c)} f(x−c) = ∏_{x∈Ico(a,b)} f(x).
LaTeX
$$$$ \\displaystyle \\prod_{x \\in \\mathrm{Ico}(a+c,b+c)} f(x-c) = \\prod_{x \\in \\mathrm{Ico}(a,b)} f(x). $$$$
Lean4
@[to_additive (attr := simp)]
theorem prod_Ico_add_right_sub_eq [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
[LocallyFiniteOrder α] [Sub α] [OrderedSub α] (a b c : α) :
∏ x ∈ Ico (a + c) (b + c), f (x - c) = ∏ x ∈ Ico a b, f x := by
simp only [← map_add_right_Ico, prod_map, addRightEmbedding_apply, add_tsub_cancel_right]
