prod_boole — Mathlib

English

The product over a Finset of booleans (represented as 0/1) equals 1 if all predicates hold, otherwise 0.

Русский

Произведение по Finset над булевыми значениями равно 1, если все предикаты истинны, иначе 0.

LaTeX

$$$\\prod_{i\\in s} \\mathrm{ite}(p(i), 1, 0) = \\mathrm{ite}\\Big(\\forall i\\in s, p(i)\\Big, 1, 0\\Big)$$$

Lean4

theorem prod_boole : ∏ i ∈ s, (ite (p i) 1 0 : M₀) = ite (∀ i ∈ s, p i) 1 0 := by rw [prod_ite_zero, prod_const_one]

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