map_update_add — Mathlib

English

Updating a single coordinate by adding u+v inside the f, then applying map distributes over the addition: map(update f i (u+v)) = map(update f i u) + map(update f i v).

Русский

Обновление одной координаты на (u+v) внутри f и применение map распределяются по сложению.

LaTeX

$$$\mathrm{map}(\mathrm{update}\ f\ i\ (u+v)) = \mathrm{map}(\mathrm{update}\ f\ i\ u) + \mathrm{map}(\mathrm{update}\ f\ i\ v)$$$

Lean4

protected theorem map_update_add [DecidableEq ι] (i : ι) (u v : s i →ₗ[R] t i) :
    map (update f i (u + v)) = map (update f i u) + map (update f i v) :=
  by
  ext x
  simp only [LinearMap.compMultilinearMap_apply, map_tprod, map_add_smul_aux, LinearMap.add_apply,
    MultilinearMap.map_update_add]

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