English
For any multiset s and function f, (s.attach.map (λ i => f i.val)) = s.map f, i.e., attaching and then mapping by taking the element value is the same as mapping the underlying multiset.
Русский
Для мультимножества s и функции f выполняется (s.attach.map (λ i. i.val)) = s.map f: прикрепление и затем отображение через взятие значения элемента эквивалентны отображению по базовому мультимножеству.
LaTeX
$$$\\forall s:\\\\mathrm{Multiset}\\\\ \\alpha,\\; \\forall f:\\\\alpha\\\\to\\\\beta,\\; (s.\\\\attach.map\\\\ (\\\\lambda i\\\\, i.\\\\val)) = s.\\\\map f.$$$
Lean4
@[simp]
theorem attach_map_val' (s : Multiset α) (f : α → β) : (s.attach.map fun i => f i.val) = s.map f :=
Quot.inductionOn s fun _ => congr_arg _ List.attach_map_val
