English
Replacing the second sequence by its image under f and then zipping with the first is the same as zipping with the second and applying g to the results after mapping f on the second argument.
Русский
Заменяя вторую последовательность её образом под f и затем зипуя с первой, получаем то же самое, что зиповать с первой и применить g к результатам после отображения на второй аргумент.
LaTeX
$$$$ \\mathrm{zipWith}\\ g\\ s_1 (\\mathrm{map}\\ f\\ s_2) = \\mathrm{zipWith}\\ (\\lambda a b \\mapsto g a (f b))\\ s_1\\ s_2. $$$$
Lean4
theorem zipWith_map_right (s₁ : Seq α) (s₂ : Seq β) (f : β → β') (g : α → β' → γ) :
zipWith g s₁ (s₂.map f) = zipWith (fun a b ↦ g a (f b)) s₁ s₂ :=
by
convert zipWith_map _ _ (@id α) _ _
simp
