pmap_next_eq_rotate_one — Mathlib

English

For a Nodup list l, mapping each element to its successor via a parallel map equals the list rotated by 1.

Русский

Для списка без повторов l сопоставление каждого элемента с его соседом по циклу через параллельное отображение равно списку, повернутому на 1.

LaTeX

$$$(l.pmap\ l.next\ (\lambda\ _\ h:\, h)) = l.rotate\ 1$$$

Lean4

theorem pmap_next_eq_rotate_one (h : Nodup l) : (l.pmap l.next fun _ h => h) = l.rotate 1 :=
  by
  apply List.ext_getElem
  · simp
  · intros
    rw [getElem_pmap, getElem_rotate, next_getElem _ h]

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