tail_update_succ — Mathlib

English

Updating a nonzero element and taking the tail commutes with tail and update: tail (update q i.succ y) = update (tail q) i y.

Русский

Обновление не нулевого элемента и взятие хвоста коммутируют с хвостом и обновлением: tail (update q i.succ y) = update (tail q) i y.

LaTeX

$$$\\mathrm{tail}(\\\\mathrm{update}(q,\\\\mathrm{succ}(i),y)) = \\\\mathrm{update}(\\\\mathrm{tail}(q),i,y)$$$

Lean4

/-- Updating a nonzero element and taking the tail commute. -/
@[simp]
theorem tail_update_succ : tail (update q i.succ y) = update (tail q) i y :=
  by
  ext j
  by_cases h : j = i
  · rw [h]
    simp [tail]
  · simp [tail, (Fin.succ_injective n).ne h, h]

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