prod_boole — Mathlib

English

For any predicate p on a finite set, the product of ite(p(i),1,0) over all i equals ite(all p(i), 1, 0).

Русский

Для конечного множеста и предиката p произведение ite(p(i),1,0) по всем i равно ite(все p(i),1,0).

LaTeX

$$$\\forall {ι} [\\mathsf{Fintype} ι] [\\mathsf{CommMonoidWithZero} M₀] (p: ι \\to \\mathsf{Prop}) [\\mathsf{DecidablePred} p], (f: ι \\to M₀),\\; \\mathrm{univ}.prod (\\lambda i, \\mathrm{ite}(p i, 1, 0)) = \\mathrm{ite}(\\forall i, p i, 1, 0)$$$

Lean4

theorem prod_boole : ∏ i, (ite (p i) 1 0 : M₀) = ite (∀ i, p i) 1 0 := by simp [Finset.prod_boole]

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