English
For a Finset s, a predicate p, and a, the product over s of ite(p i) a 1 equals ite(exists i∈s, p i) a 1.
Русский
Для множества s и предиката p, а также константы a, произведение по i∈s of ite(p i) a 1 равно ite(существует i∈s, p i) a 1.
LaTeX
$$$\\displaystyle \\prod_{i \\in s} \\operatorname{ite}(p(i))\,a\,1 = \\operatorname{ite}\\left(\\exists i \\in s, p(i)\\right) a 1$$$
Lean4
/-- See also `Finset.prod_ite_zero`. -/
@[to_additive /-- See also `Finset.sum_boole`. -/
]
theorem prod_ite_one (s : Finset ι) (p : ι → Prop) [DecidablePred p] (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : M) :
∏ i ∈ s, ite (p i) a 1 = ite (∃ i ∈ s, p i) a 1 :=
by
split_ifs with h
· obtain ⟨i, hi, hpi⟩ := h
rw [prod_eq_single_of_mem _ hi, if_pos hpi]
exact fun j hj hji ↦ if_neg fun hpj ↦ hji <| h _ hj _ hi hpj hpi
· push_neg at h
rw [prod_eq_one]
exact fun i hi => if_neg (h i hi)
