finRange_map_get — Mathlib

English

For any list l, the list obtained by taking finRange of its length and mapping its elements by l.get yields l itself: (finRange (length l)).map l.get = l.

Русский

Для любого списка l получается, что список, полученный применением l.get к каждому индексу из finRange(length l), равен самому списку: (finRange (length l)).map l.get = l.

LaTeX

$$$$ (finRange\\,\\text{length}(l)).map\\, l\\text{.get} = l. $$$$

Lean4

@[simp]
theorem finRange_map_get (l : List α) : (finRange l.length).map l.get = l :=
  List.ext_get (by simp) (by simp)

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