English
If i is a member of s, then updating the piecewise function at i by v yields the same result as updating only the left branch: update(s.piecewise f g) i v = s.piecewise (update f i v) g.
Русский
Если i ∈ s, то обновление кусочно-заданной функции по i и значению v эквивалентно обновлению только левой ветви: update(s.piecewise f g) i v = s.piecewise (update f i v) g.
LaTeX
$$$$\\text{If } i \\in s,\\quad update\\bigl(s.piecewise f g\\bigr) i v = s.piecewise (update f i v)\\; g.$$$$
Lean4
theorem update_piecewise_of_mem [DecidableEq ι] {i : ι} (hi : i ∈ s) (v : π i) :
update (s.piecewise f g) i v = s.piecewise (update f i v) g :=
by
rw [update_piecewise]
refine s.piecewise_congr (fun _ _ => rfl) fun j hj => update_of_ne ?_ ..
exact fun h => hj (h.symm ▸ hi)
