finRange_map_getElem — Mathlib

English

For any list l, the list consisting of the elements l at every index (indexed by Fin l.length) equals l: (finRange l.length).map (l[·.1]) = l.

Русский

Для любого списка l последовательность его элементов по всем индексам (индексирование Fin l.length) равна самому списку: (finRange l.length).map (l[·.1]) = l.

LaTeX

$$$$ (finRange\\,l.length).map\\ (\\lambda i: l[i]) = l. $$$$

Lean4

@[simp]
theorem finRange_map_getElem (l : List α) : (finRange l.length).map (l[·.1]) = l :=
  finRange_map_get l

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