zip_map_left — Mathlib

English

Zipping a mapped first sequence with a second is the same as zipping the original first sequence with the second and mapping with Prod.map on the left component.

Русский

Зипование отображённой первой последовательности с второй равно зипованию исходной первой последовательности с второй и отображению левой части через Prod.map.

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 zip_map_left (s₁ : Seq α) (s₂ : Seq β) (f : α → α') : (s₁.map f).zip s₂ = (s₁.zip s₂).map (Prod.map f id) :=
  by
  convert zip_map _ _ _ _
  simp

Похожие утверждения