map_update_update — Mathlib

English

Applying two successive updates to a vector yields zero, in the alternating context.

Русский

Применение двух последовательных обновлений к вектору даёт нуль в контексте чередующейся карты.

LaTeX

$$f(Function.update(Function.update(v,i,m), j,m)) = 0$$

Lean4

theorem map_update_update [DecidableEq ι] {i j : ι} (hij : i ≠ j) (m : M) :
    f (Function.update (Function.update v i m) j m) = 0 :=
  f.map_eq_zero_of_eq _ (by rw [Function.update_self, Function.update_of_ne hij, Function.update_self]) hij

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