tail — Mathlib

English

The ith element of a vector is obtained from the underlying list at the position corresponding to i after adjusting by the length proof.

Русский

i-й элемент вектора получается из соответствующей позиции в списке с учётом доказательства длины.

LaTeX

$$$\\mathrm{get}(l, i) = l.1.\\mathrm{get}(i.cast(l.2.symm))$$$

Lean4

/-- The tail of a vector, with an empty vector having empty tail. -/
def tail : Vector α n → Vector α (n - 1)
  | ⟨[], h⟩ => ⟨[], congrArg pred h⟩
  | ⟨_ :: v, h⟩ => ⟨v, congrArg pred h⟩

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