English
Let p be a predicate on ι with decidablePred. Then the product over s with p a equals the product over s of the corresponding ite expression.
Русский
Пусть p — предикат на ι с разрешимой предикатностью. Тогда произведение по s с p a равно произведению по s от выражения if p a then f a else 1.
LaTeX
$$$\prod a\in s with p a, f a = \prod a\in s, \; \mathrm{ite}(p a, f a, 1)$$$
Lean4
@[to_additive]
theorem prod_filter (p : ι → Prop) [DecidablePred p] (f : ι → M) :
∏ a ∈ s with p a, f a = ∏ a ∈ s, if p a then f a else 1 :=
calc
∏ a ∈ s with p a, f a = ∏ a ∈ s with p a, if p a then f a else 1 :=
prod_congr rfl fun a h => by rw [if_pos]; simpa using (mem_filter.1 h).2
_ = ∏ a ∈ s, if p a then f a else 1 := by
{
refine prod_subset (filter_subset _ s) fun x hs h => ?_
rw [mem_filter, not_and] at h
exact if_neg (by simpa using h hs)
}
