snoc_init_self — Mathlib

English

Let q be a tuple of length n+1. Then the tuple obtained by taking its initial n entries and appending the last element recovers the original tuple.

Русский

Пусть q — кортеж длины n+1. Тогда кортеж, полученный из первой n элементов и добавлением последнего элемента, восстанавливает исходный кортеж.

LaTeX

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

Lean4

/-- Concatenating the first element of a tuple with its tail gives back the original tuple -/
@[simp]
theorem snoc_init_self : snoc (init q) (q (last n)) = q :=
  by
  ext j
  cases j using Fin.lastCases <;> simp [init]

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