map — Mathlib

English

Given a function f: α → β, Fin m → α maps to Fin m → β by applying f coordinatewise, i.e., map f v = seq (λ _ => f) v, so (map f v)(i) = f(v(i)).

Русский

Пусть f: α → β. Отображение вектора по координатам задаётся как map f v = seq (λ _ => f) v, то есть (map f v)(i) = f(v(i)).

LaTeX

$$$\mathrm{map}_m(f)(v) = (i \mapsto f(v(i)))$$$

Lean4

/-- `FinVec.map f v = ![f (v 0), f (v 1), ...]` -/
def map (f : α → β) {m} : (Fin m → α) → Fin m → β :=
  seq fun _ => f

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