prod_pow_boole — Mathlib

English

Let s be a finite set, f: ι → M, and a ∈ ι. Then the product over s of f(x) raised to ite(a = x) 1 0 equals ite(a ∈ s) f(a) 1.

Русский

Пусть s — конечное множество, f: ι → M, и a ∈ ι. Тогда произведение по x∈s f(x)^{ite(a = x) 1 0} равно ite(a ∈ s) f(a) 1.

LaTeX

$$$\\displaystyle \\prod_{x \\in s} f(x)^{\\operatorname{ite}(a=x)\\,1\\,0} = \\operatorname{ite}(a \\in s)\\,f(a)\\,1$$$

Lean4

@[to_additive sum_boole_nsmul]
theorem prod_pow_boole [DecidableEq ι] (s : Finset ι) (f : ι → M) (a : ι) :
    (∏ x ∈ s, f x ^ ite (a = x) 1 0) = ite (a ∈ s) (f a) 1 := by simp

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