update_snoc_last — Mathlib

English

Same as above; the update-snoc commutes: snoc (update p i y) x = update (snoc p x) i.castSucc y.

Русский

То же самое: коммутативность обновления и добавления в конец: snoc (update p i y) x = update (snoc p x) i.castSucc y.

LaTeX

$$$\\mathrm{snoc}\\ (\\mathrm{update}\\ p\\ i\\ y)\\ x = \\mathrm{update}\\ (\\mathrm{snoc}\\ p\\ x)\\ i.castSucc\\ y$$$

Lean4

/-- Adding an element at the beginning of a tuple and then updating it amounts to adding it
directly. -/
theorem update_snoc_last : update (snoc p x) (last n) z = snoc p z :=
  by
  ext j
  cases j using lastCases <;> simp

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