update_eq_updateFinset — Mathlib

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]

Похожие утверждения