English
For s, f and x, the map of f over s.attach.erase x equals the erase of x in s mapped by f, i.e., (s.attach.erase x).map f = (s.erase x).map f (under suitable rewriting).
Русский
Для s, f и x отображение через f над s.attach.erase x эквивалентно erase x из s, затем отображение через f.
LaTeX
$$$\\forall s:\\\\mathrm{Multiset}\\\\ \\alpha,\\\\forall f:\\\\alpha\\\\to\\\\beta,\\\\forall x:{ x\\\\in s },\\\\ (s.\\\\attach.\\\\erase x).\\\\map (\\\\lambda j:\\\\, j) = (s.\\\\erase x).\\\\map f.$$$
Lean4
theorem erase_attach_map (s : Multiset α) (f : α → β) (x : { x // x ∈ s }) :
(s.attach.erase x).map (fun j : { x // x ∈ s } ↦ f j) = (s.erase x).map f :=
by
simp only [← Function.comp_apply (f := f)]
rw [← map_map, erase_attach_map_val]
