English
If b = 0, then update behaves like erase; otherwise it inserts i into the support.
Русский
Если b = 0, обновление эквивалентно удалению; иначе оно вставляет i в опору.
LaTeX
$$$\\operatorname{support}(f.update\\ i\\ b) = \\begin{cases} \\operatorname{support}(f.erase i) & \\text{if } b = 0 \\\\ \\operatorname{insert} i\\ f.{\\mathrm{support}} & \\text{otherwise} \\end{cases}$$$
Lean4
theorem support_update (f : Π₀ i, β i) (i : ι) (b : β i) [Decidable (b = 0)] :
support (f.update i b) = if b = 0 then support (f.erase i) else insert i f.support :=
by
ext j
split_ifs with hb
· subst hb
simp [update_eq_erase, support_erase]
· rw [support_update_ne_zero f _ hb]
