map_update — Mathlib

English

A fundamental identity relates updating an input and subtracting a shifted version of the input.

Русский

Основное тождество связывает обновление входа и вычитание смещённой версии входа.

LaTeX

$$$$f(\\text{update } x\, i\, v) = f(x) - f(\\text{update } x\, i\, (x_i - v)).$$$$

Lean4

theorem map_update [DecidableEq ι] (x : (i : ι) → M₁ i) (i : ι) (v : M₁ i) :
    f (update x i v) = f x - f (update x i (x i - v)) := by rw [map_update_sub, update_eq_self, sub_sub_cancel]

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