English
Inserting j into s yields a piecewise equal to updating by f(j) at j: (insert j s).piecewise f g = update (s.piecewise f g) j (f j).
Русский
Добавление j в s даёт piecewise, равное обновлению в точке j значением f(j).
LaTeX
$$$(\\mathrm{insert}\\ j\\ s).\\text{piecewise } f g = \\mathrm{update} (s.\\text{piecewise } f g)\\ j\\ (f\\ j).$$$
Lean4
theorem piecewise_insert [DecidableEq ι] (j : ι) [∀ i, Decidable (i ∈ insert j s)] :
(insert j s).piecewise f g = update (s.piecewise f g) j (f j) :=
by
classical simp only [← piecewise_coe, ← Set.piecewise_insert]
ext
congr
simp