zip_map — Mathlib

English

Zipping two mapped sequences is the same as mapping the zip of the original sequences with the pairwise product map.

Русский

Зипование двух отображённых последовательностей эквивалентно отображению результата зипа исходных последовательностей функцией, применяющей к паре.

LaTeX

$$$$ (s_1.map f_1) \\; \\mathrm{zip} \\; (s_2.map f_2) = (s_1 \\; \\mathrm{zip} \\; s_2).map (\\mathrm{Prod.map} f_1 f_2). $$$$

Lean4

theorem zip_map (s₁ : Seq α) (s₂ : Seq β) (f₁ : α → α') (f₂ : β → β') :
    (s₁.map f₁).zip (s₂.map f₂) = (s₁.zip s₂).map (Prod.map f₁ f₂) :=
  by
  ext1 n
  simp
  cases s₁.get? n <;> cases s₂.get? n <;> simp

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