map_update_sub — Mathlib

English

For any index i and elements x,y in the i-th factor, replacing the i-th coordinate by x − y inside the argument of f yields f(update m i (x − y)) = f(update m i x) − f(update m i y).

Русский

Для любого индекса i и элементов x,y в i‑й координате, замена i‑й координаты на x − y внутри аргумента f даёт равенство f(update m i (x − y)) = f(update m i x) − f(update m i y).

LaTeX

$$$f\bigl(\mathrm{update}\,m\,i\,(x- y)\bigr) = f\bigl(\mathrm{update}\,m\,i\,x\bigr) - f\bigl(\mathrm{update}\,m\,i\,y\bigr)$$$

Lean4

@[simp]
theorem map_update_sub [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (x y : M₁ i) :
    f (update m i (x - y)) = f (update m i x) - f (update m i y) :=
  f.toMultilinearMap.map_update_sub _ _ _ _

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