English
For any g: α→β and h: β→Gγ with G applicative commuting, and x: Multiset α, traverse h (map g x) = traverse (h ∘ g) x.
Русский
Для любых g и h и x: Multiset α выполняется равенство обхода и отображения.
LaTeX
$$$\\mathrm{traverse} h\\big(\\mathrm{map} g\\ x\\big) = \\mathrm{traverse}(h \\circ g)\\ x$$$
Lean4
theorem traverse_map {G : Type* → Type _} [Applicative G] [CommApplicative G] {α β γ : Type _} (g : α → β) (h : β → G γ)
(x : Multiset α) : traverse h (map g x) = traverse (h ∘ g) x :=
by
refine Quotient.inductionOn x ?_
intro
simp only [traverse, quot_mk_to_coe, map_coe, lift_coe, Function.comp_apply]
rw [← Traversable.traverse_map h g, List.map_eq_map]
