support_update_zero — Mathlib

English

When updating at a with 0, the support of f.update a 0 equals f.support erase a.

Русский

При обновлении по a на 0 опора функции равна опоре исходной функции за вычетом элемента a.

LaTeX

$$$\operatorname{supp}(f.update(a,0)) = \operatorname{supp}(f) \setminus \{a\}$$$

Lean4

@[simp]
theorem support_update_zero [DecidableEq α] : support (f.update a 0) = f.support.erase a := by
  classical
  simp only [update, ite_true]
  congr!

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