English
Let s be a finite subset of an index type ι, and f,g be families of values indexed by ι. Then for every i and v, the update of the piecewise function s.piecewise f g at i by v equals the piecewise function formed from the pointwise updates: update(s.piecewise f g) i v = s.piecewise (update f i v) (update g i v).
Русский
Пусть s — конечное подмножество индексов ι, а f, g — семейства значений, индексируемые по ι. Тогда для любых i и v выполняется обновление функции s.piecewise f g по i значению v равно кусочно-заданной функции, полученной из точечных обновлений: update(s.piecewise f g) i v = s.piecewise (update f i v) (update g i v).
LaTeX
$$$$\\operatorname{update}\\bigl(s.piecewise f g\\bigr)\\ i\\ v = s.piecewise\\bigl(\\operatorname{update} f\\ i\\ v\\bigr)\\bigl(\\operatorname{update} g\\ i\\ v\\bigr).$$$$
Lean4
theorem update_piecewise [DecidableEq ι] (i : ι) (v : π i) :
update (s.piecewise f g) i v = s.piecewise (update f i v) (update g i v) :=
by
ext j
rcases em (j = i) with (rfl | hj) <;> by_cases hs : j ∈ s <;> simp [*]
