zip_cons_cons — Mathlib

English

Zipping two sequences both built with cons preserves the pairwise structure: the result is a sequence starting with the pair of the heads, followed by the zip of the tails.

Русский

Зипование двух последовательностей, построенных как cons, сохраняет попарную структуру: результат начинается парой голов, затем следует зип хвостов.

LaTeX

$$$$ \\mathrm{zipWith}\\ f\\ (\\mathrm{cons}\\ x\\ s) (\\mathrm{cons}\\ x'\\ s') = \\mathrm{cons}\\ (f\\ x\\ x')\\ (\\mathrm{zipWith}\\ f\\ s\\ s'). $$$$

Lean4

@[simp]
theorem zip_cons_cons {s s' : Seq α} {x x'} : zip (cons x s) (cons x' s') = cons (x, x') (zip s s') :=
  zipWith_cons_cons

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