English
Let m be a multiset of ι, f a function on the subtype {x ∈ m} into M, and g: ι → M with f x = g x for every x in the corresponding subtype. Then the product over the universe equals the product over m's finite representation: ∏_{x ∈ univ} f x = ∏_{x ∈ m.toFinset} g x.
Русский
Пусть m — мульти множество ι, f: {x ∈ m} → M, g: ι → M и f x = g x на соответствующем подтипе. Тогда произведение по всему множеству равно произведению по представлению m в виде конечного множества: ∏_{x ∈ univ} f x = ∏_{x ∈ m.toFinset} g x.
LaTeX
$$$\\forall m:\\, \\text{Multiset } ι\\; (f:\\{x \\mid x \\in m\\} \\to M)\\; (g:ι \\to M)\\; (hfg: ∀ x, f x = g x)\\; ⇒\\; Eq (Finset.univ.prod (λ x, f x)) (m.toFinset.prod (λ x, g x))$$$
Lean4
theorem sum_filter_count_eq_countP [DecidableEq ι] (p : ι → Prop) [DecidablePred p] (l : List ι) :
∑ x ∈ l.toFinset with p x, l.count x = l.countP p := by simp [Finset.sum, sum_map_count_dedup_filter_eq_countP p l]
