init_update_last — Mathlib

English

Updating the last element of a Fin-tuple does not change its beginning.

Русский

Обновление последнего элемента кортежа Fin не изменяет его префикс.

LaTeX

$$$\\\\operatorname{init}(\\\\operatorname{update} q(\\\\mathrm{last} \\\\; n) z) = \\\\operatorname{init} q$$$

Lean4

/-- Updating the last element of a tuple does not change the beginning. -/
@[simp]
theorem init_update_last : init (update q (last n) z) = init q :=
  by
  ext j
  simp [init, Fin.ne_of_lt]

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