map' — Mathlib

English

The map operation on a vector of functors is defined pointwise by applying map f to each component.

Русский

Операция отображения на векторе функторов задаётся поэтапно, применяя к каждому компоненту отображение map f.

LaTeX

$$$\mathrm{map}'(f) = \lambda (g_i)_{i}, \; (i \mapsto (\mathrm{G}_i) \mathrm{map} f)(g_i)_{i}.$$$

Lean4

/-- map operation defined on a vector of functors -/
protected def map' : (fun i : Fin2 n ↦ G i α) ⟹ fun i : Fin2 n ↦ G i β := fun _i ↦ map f

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