map_update_self — Mathlib

English

If you update a vector by itself at a single index, the result interacts with the alternating property to vanish under certain conditions.

Русский

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

LaTeX

$$f.updateSelf i j m = 0$$

Lean4

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

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