English
Given a multiset m of elements of ι, a function f on the subtype {x // x ∈ m} to M and a function g: ι → M, if f(x) = g(x) for all x in the subtype, then the product over the subtype equals the product over m converted to a finite set of g-values: ∏ x:{x ∈ m} f x = ∏ x ∈ m.toFinset, g x.
Русский
Пусть m — мультимножество элементов ι, f на подкласс {x | x ∈ m} в M и g: ι → M; если f x = g x для всех x в подмножестве, то произведение по подмножеству равно произведению по мультимножесту значений g:
LaTeX
$$$\prod x : \{ x \mid x \in m \}, f x = \prod x \in m.\toFinset, g x$$$
Lean4
@[to_additive]
theorem prod_mem_multiset [DecidableEq ι] (m : Multiset ι) (f : { x // x ∈ m } → M) (g : ι → M) (hfg : ∀ x, f x = g x) :
∏ x : { x // x ∈ m }, f x = ∏ x ∈ m.toFinset, g x := by
refine prod_bij' (fun x _ ↦ x) (fun x hx ↦ ⟨x, Multiset.mem_toFinset.1 hx⟩) ?_ ?_ ?_ ?_ ?_ <;> simp [hfg]
