English
Let g: α → G β and h: β → γ be functions, and s a Finset α. Then applying map h to the results of traversing s with g is the same as traversing s with the composed map h ∘ g.
Русский
Пусть g: α → G β и h: β → γ, и s — конечное множество α. Тогда отображение результатов обходa (traverse) по g и затем применением h к полученным значениям эквивалентно обходу по композиции h ∘ g.
LaTeX
$$$ \operatorname{map} \; h \langle \mathrm{traverse}\; g\; s \rangle = \mathrm{traverse}(\operatorname{map} \; h \circ g)\, s $$$
Lean4
theorem map_traverse (g : α → G β) (h : β → γ) (s : Finset α) :
Functor.map h <$> traverse g s = traverse (Functor.map h ∘ g) s :=
by
unfold traverse
simp only [Functor.map_map, fmap_def, map_comp_coe_apply, Multiset.fmap_def, ← Multiset.map_traverse]
