get_map — Mathlib

English

Mapping a function over a vector commutes with the get operation: the i-th element of v.map f equals f applied to the i-th element of v.

Русский

Отображение функции на векторе коммутирует операцию получения: i-й элемент (v.map f) равен f(v[i]).

LaTeX

$$$\forall v:\mathrm{Vector}\,\alpha\,n\;\forall f:\alpha\to\beta\;\forall i:\mathrm{Fin}\,n,\; (v.map\ f).get\ i = f( v.get\ i )$$$

Lean4

@[simp]
theorem get_map {β : Type*} (v : Vector α n) (f : α → β) (i : Fin n) : (v.map f).get i = f (v.get i) := by cases v;
  simp [Vector.map, get_eq_get_toList]

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