image_multiset_prod — Mathlib

English

Extending the list case to multisets, the image of the multiset product equals the multiset product of images.

Русский

Расширяя на мультимножества, образ произведения мультимножества равен произведению образов.

LaTeX

$$Set.image (f) (Multiset.prod t) = Multiset.map (fun s => Set.image f s) t).prod$$

Lean4

@[to_additive]
theorem image_multiset_prod (f : F) : ∀ m : Multiset (Set α), (f : α → β) '' m.prod = (m.map fun s => f '' s).prod :=
  Quotient.ind <| by simpa only [Multiset.quot_mk_to_coe, Multiset.prod_coe, Multiset.map_coe] using image_list_prod f

Похожие утверждения