prod_ite_eq — Mathlib

English

Given a finite set s, an index a, and a family b, the product over s of ite (a = x) (b x) 1 equals the piecewise expression depending on whether a ∈ s.

Русский

С учётом конечности s, произведение ite (a = x) (b x) 1 равно произведению, которое зависит от того, принадлежит ли a s.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem prod_ite_eq [DecidableEq ι] (s : Finset ι) (a : ι) (b : ι → M) :
    (∏ x ∈ s, ite (a = x) (b x) 1) = ite (a ∈ s) (b a) 1 :=
  prod_dite_eq s a fun x _ => b x

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