Lean4
/-- Replace the value of a `α →₀ M` at a given point `a : α` by a given value `b : M`.
If `b = 0`, this amounts to removing `a` from the `Finsupp.support`.
Otherwise, if `a` was not in the `Finsupp.support`, it is added to it.
This is the finitely-supported version of `Function.update`. -/
def update (f : α →₀ M) (a : α) (b : M) : α →₀ M
where
support := by
haveI := Classical.decEq α; haveI := Classical.decEq M
exact if b = 0 then f.support.erase a else insert a f.support
toFun :=
haveI := Classical.decEq α
Function.update f a b
mem_support_toFun
i := by
classical
rw [Function.update]
simp only [eq_rec_constant, dite_eq_ite, ne_eq]
split_ifs with hb ha ha <;> try simp only [*, not_false_iff, iff_true, not_true, iff_false]
· rw [Finset.mem_erase]
simp
· rw [Finset.mem_erase]
simp [ha]
· rw [Finset.mem_insert]
simp
· rw [Finset.mem_insert]
simp [ha]
