prod_update_of_notMem — Mathlib

English

If i ∉ s, then updating f at i does not change the product over s: ∏ x∈s, update f i b x = ∏ x∈s, f x.

Русский

Если i не принадлежит s, то замена значения f на i на произвольное b не изменяет произведение по s: ∏_{x∈s} (update f i b x) = ∏_{x∈s} f x.

LaTeX

$$$\\displaystyle \\prod_{x \\in s} \\mathrm{Function.update}\\, f\\, i\\, b\\, x = \\prod_{x \\in s} f(x)$$$

Lean4

@[to_additive]
theorem prod_update_of_notMem [DecidableEq ι] {s : Finset ι} {i : ι} (h : i ∉ s) (f : ι → M) (b : M) :
    ∏ x ∈ s, Function.update f i b x = ∏ x ∈ s, f x :=
  by
  apply prod_congr rfl
  intro j hj
  have : j ≠ i := by
    rintro rfl
    exact h hj
  simp [this]

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