English
For s, f, t as in the lemma, the product over s of (t i).mulIndicator (f i) (g i) equals the product over i ∈ s with g(i) ∈ t(i) of f(i)(g(i)).
Русский
Произведение по i∈s индикации множителя равно произведению по всем i, удовлетворяющим g(i) ∈ t(i).
LaTeX
$$$\prod i \in s, (t(i).mulIndicator (f(i)) (g(i))) = \prod i \in s, \mathbf{1}_{g(i) \in t(i)} f(i)(g(i))$$$
Lean4
@[to_additive]
theorem prod_mulIndicator_eq_prod_filter (s : Finset ι) (f : ι → κ → β) (t : ι → Set κ) (g : ι → κ)
[DecidablePred fun i ↦ g i ∈ t i] : ∏ i ∈ s, mulIndicator (t i) (f i) (g i) = ∏ i ∈ s with g i ∈ t i, f i (g i) :=
by
refine
(prod_filter_mul_prod_filter_not s (fun i ↦ g i ∈ t i) _).symm.trans <|
Eq.trans (congr_arg₂ (· * ·) ?_ ?_) (mul_one _)
· exact prod_congr rfl fun x hx ↦ mulIndicator_of_mem (mem_filter.1 hx).2 _
· exact prod_eq_one fun x hx ↦ mulIndicator_of_notMem (mem_filter.1 hx).2 _
