zipWith_rotate_one — Mathlib

English

For any f, x, y and list l, the zipWith of (x :: y :: l) with its rotation by 1 equals a list whose head is f x y and whose tail is zipWith f (y :: l) (l ++ [x]).

Русский

Для любого f, x, y и списка l, zipWith f применён к (x :: y :: l) и к его повороту на 1 равно списку, у которого головной элемент f x y, а хвост равен zipWith f (y :: l) (l ++ [x]).

LaTeX

$$$\\mathrm{zipWith} f (x \\textasciitli y \\ell) ((x \\textasciitli y \\ell).rotate 1) = x\\! \\text{??}$$$

Lean4

theorem zipWith_rotate_one {β : Type*} (f : α → α → β) (x y : α) (l : List α) :
    zipWith f (x :: y :: l) ((x :: y :: l).rotate 1) = f x y :: zipWith f (y :: l) (l ++ [x]) := by simp

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