getElem_map — Mathlib

English

Mapping commutes with element access: the i-th element of the mapped vector equals the image under f of the i-th element, for i less than n.

Русский

Обращение к элементу после отображения равно образу элемента до отображения: (v.map f)[i] = f(v[i]).

LaTeX

$$$(v.map f)[i] = f\\,v[i]$ при $i < n$$$

Lean4

@[simp]
theorem getElem_map {β : Type*} (v : Vector α n) (f : α → β) {i : ℕ} (hi : i < n) : (v.map f)[i] = f v[i] := by
  simp only [getElem_def, toList_map, List.getElem_map]

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