updateFinset_singleton — Mathlib

English

If s = {i}, then updateFinset x {i} y equals the standard update of coordinate i to y.

Русский

Если s = {i}, то updateFinset x {i} y равняется обычному обновлению координаты i значением y.

LaTeX

$$$\\text{updateFinset}\\;x\\;\\{i\\}\\;y = \\text{update}\\;x\\;i\\; (y\\langle i, \\text{mem_singleton_self } i \\rangle)$$$

Lean4

theorem updateFinset_singleton {i y} : updateFinset x { i } y = Function.update x i (y ⟨i, mem_singleton_self i⟩) :=
  by
  congr with j
  by_cases hj : j = i
  · cases hj
    simp only [dif_pos, Finset.mem_singleton, update_self, updateFinset]
  · simp [hj, updateFinset]

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