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