vector_tail — Mathlib

English

The tail (vector without the first element) is primitive recursive.

Русский

Хвост вектора — хвостовой вектор без первого элемента — примитивно-рекурсивен.

LaTeX

$$$$ \\operatorname{Primrec}\\big( \\mathrm{List.Vector.tail} : \\mathrm{List.Vector}\\ \\alpha\\ n \\to \\mathrm{List.Vector}\\ \\alpha\\ (n-1) \\big). $$$$

Lean4

theorem vector_tail {n} : Primrec (@List.Vector.tail α n) :=
  vector_toList_iff.1 <| (list_tail.comp vector_toList).of_eq fun ⟨l, h⟩ => by cases l <;> rfl

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