prod_ite_eq_of_mem' — Mathlib

English

A variant asserting the same equality with a different presentation of arguments.

Русский

Вариант утвердующий ту же самую равенство с другим представлением аргументов.

LaTeX

$$$\\prod_{x \\in s} (\\text{ite}(x = a) (b x) 1) = \\text{ite}(a \\in s) (b a) 1$.$$

Lean4

/-- The difference with `Finset.prod_ite_eq_of_mem` is that the arguments to `Eq` are swapped. -/
@[to_additive]
theorem prod_ite_eq_of_mem' [DecidableEq ι] (s : Finset ι) (a : ι) (b : ι → M) (h : a ∈ s) :
    (∏ x ∈ s, if x = a then b x else 1) = b a := by simp only [prod_ite_eq', if_pos h]

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