map_update_neg — Mathlib

English

Changing the i-th input by negation corresponds to negating the output of the updated input map.

Русский

Замена i-го аргумента на −x приводит к тому, что значение отображения становится противоположным.

LaTeX

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

Lean4

@[simp]
theorem map_update_neg [DecidableEq ι] (m : ∀ i, M₁ i) (i : ι) (x : M₁ i) : f (update m i (-x)) = -f (update m i x) :=
  eq_neg_of_add_eq_zero_left <| by
    rw [← MultilinearMap.map_update_add, neg_add_cancel, f.map_coord_zero i (update_self i 0 m)]

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