English
Let m be a multiset, n a multiset, and f a function of two arguments. The iterated map distributes: prod(map (i => prod (n.map (j => f i j))) m) = prod(map (j => prod (m.map (i => f i j))) n).
Русский
Пусть m и n – мультимножества, f двумерная функция. Произведение распределяется: prod(map i => prod (n.map j => f i j)) m = prod(map j => prod (m.map i => f i j)) n.
LaTeX
$$$ \mathrm{prod}(\mathrm{map}(\lambda i. \mathrm{prod}(\mathrm{map}(\lambda j. f\ i\ j)\, n))\, m) = \mathrm{prod}(\mathrm{map}(\lambda j. \mathrm{prod}(\mathrm{map}(\lambda i. f\ i\ j)\, m))\, n) $$$
Lean4
@[to_additive]
theorem prod_map_prod_map (m : Multiset ι) (n : Multiset κ) {f : ι → κ → M} :
prod (m.map fun a => prod <| n.map fun b => f a b) = prod (n.map fun b => prod <| m.map fun a => f a b) :=
Multiset.induction_on m (by simp) fun a m ih => by simp [ih]
