English
For a predicate p on α and functions f, g: α → M, the product of the map that chooses f or g according to p equals the product over those elements satisfying p of f and those not satisfying p of g.
Русский
Для предиката p на α и функций f, g: α → M произведение отображённой функции, выбирающей f или g по p, равно произведению по элементам, удовлетворяющим p, от f и по элементам, не удовлетворяющим p, от g.
LaTeX
$$$ \bigl(\mathrm{map} (\lambda a, \; \text{ite } (p a) (f a) (g a))\; l\bigr).prod =\n (\mathrm{map} f (\mathrm{filter} (\lambda a, \; \mathrm{decide} (p a)) l)).prod \cdot (\mathrm{map} g (\mathrm{filter} (\lambda a, \; \mathrm{decide} (Not (p a))) l)).prod $$$
Lean4
@[to_additive]
theorem prod_map_ite (p : α → Prop) [DecidablePred p] (f g : α → M) (l : List α) :
(l.map fun a => if p a then f a else g a).prod = ((l.filter p).map f).prod * ((l.filter fun a ↦ ¬p a).map g).prod :=
by
induction l with
| nil => simp
| cons x xs ih =>
simp only [map_cons, filter_cons, prod_cons] at ih ⊢
rw [ih]
clear ih
by_cases hx : p x
·
simp only [hx, ↓reduceIte, decide_not, decide_true, map_cons, prod_cons, not_true_eq_false, decide_false,
Bool.false_eq_true, mul_assoc]
·
simp only [hx, ↓reduceIte, decide_not, decide_false, Bool.false_eq_true, not_false_eq_true, decide_true, map_cons,
prod_cons, mul_left_comm]
