prod_ite_mem — Mathlib

English

If ι is finite, then the product of a conditional over s reduces to the product over the intersection with s and the membership predicate.

Русский

Поскольку ι конечен, произведение по условной функции сводится к произведению по пересечению с s и принадлежности.

LaTeX

$$$\\prod i \\in s, (\\text{if } i \\in t \\text{ then } f i \\text{ else } 1) = \\prod i \\in s \\cap t, f i$.$$

Lean4

@[to_additive (attr := simp)]
theorem prod_ite_mem [DecidableEq ι] (s t : Finset ι) (f : ι → M) :
    ∏ i ∈ s, (if i ∈ t then f i else 1) = ∏ i ∈ s ∩ t, f i := by rw [← Finset.prod_filter, Finset.filter_mem_eq_inter]

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