snoc_update — Mathlib

English

Updating an element in the left part commutes with snoc: snoc (update p i y) x = update (snoc p x) i.castSucc y.

Русский

Обновление элемента слева конмутирует snoc: 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

/-- Updating a tuple and adding an element at the end commute. -/
@[simp]
theorem snoc_update : snoc (update p i y) x = update (snoc p x) i.castSucc y :=
  by
  ext j
  cases j using lastCases with
  | cast j => rcases eq_or_ne j i with rfl | hne <;> simp [*]
  | last => simp [Ne.symm]

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