pmap_prev_eq_rotate_length_sub_one

English

In a Nodup list l, mapping each element to its predecessor yields the list rotated by length(l) - 1.

Русский

В списке без повторов pmap с предшественником даёт список, повернутый на length(l) - 1.

LaTeX

$$$(l.pmap\ l.prev\ (\lambda\ _ h:\ h)) = l.rotate\ (l.length - 1)$$$

Lean4

theorem pmap_prev_eq_rotate_length_sub_one (h : Nodup l) : (l.pmap l.prev fun _ h => h) = l.rotate (l.length - 1) :=
  by
  apply List.ext_getElem
  · simp
  · intro n hn hn'
    rw [getElem_rotate, getElem_pmap, prev_getElem _ h]

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