English
Zipping two sequences after mapping each with possibly different functions is equal to mapping the result of zipping with a combined function.
Русский
Зипование двух последовательностей после отображения каждой функцией даёт те же результаты, что и отображение комбинации функций после зипа.
LaTeX
$$$$ \\mathrm{zipWith}\\ g (s_1.map f_1) (s_2.map f_2) = \\mathrm{zipWith}\\ (\\lambda a b \\mapsto g (f_1\\ a) (f_2\\ b))\\ s_1\\ s_2. $$$$
Lean4
theorem zipWith_map (s₁ : Seq α) (s₂ : Seq β) (f₁ : α → α') (f₂ : β → β') (g : α' → β' → γ) :
zipWith g (s₁.map f₁) (s₂.map f₂) = zipWith (fun a b ↦ g (f₁ a) (f₂ b)) s₁ s₂ :=
by
ext1 n
simp only [get?_zipWith, map_get?]
cases s₁.get? n <;> cases s₂.get? n <;> simp
