zip_map_right — Mathlib

English

Zipping a first sequence with a mapped second sequence is the same as zipping the first sequence with the second and mapping on the right component.

Русский

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

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

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