support_update_ne_zero — Mathlib

English

If b ≠ 0, then support of f.update a b equals insert a f.support.

Русский

Если b ≠ 0, то опора обновления равна вставке a в опору исходной функции.

LaTeX

$$$\operatorname{supp}(f.update(a,b)) = \operatorname{insert}(a, \operatorname{supp}(f))$$$

Lean4

theorem support_update_ne_zero [DecidableEq α] (h : b ≠ 0) : support (f.update a b) = insert a f.support := by
  classical
  simp only [update, h, ite_false]
  congr!

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