English
The generic update of coordinate i is equal to updating with the singleton {i} and the uniqueElim of y.
Русский
Общее обновление координаты i эквивалентно обновлению по одиночному множеству {i} и uniqueElim.
LaTeX
$$$\\text{update}\\;x\\;i\\;y = \\text{updateFinset}\\;x\\;\\{i\\}\\; (\\text{uniqueElim } y)$$$
Lean4
theorem update_eq_updateFinset {i y} : Function.update x i y = updateFinset x { i } (uniqueElim y) :=
by
congr with j
by_cases hj : j = i
· cases hj
simp only [dif_pos, Finset.mem_singleton, update_self, updateFinset]
exact uniqueElim_default (α := fun j : ({ i } : Finset ι) => π j) y
· simp [hj, updateFinset]