tail — Mathlib

English

The tail of an (n+1)-tuple q is the n-tuple obtained by discarding the first entry: tail q(i) = q(i.succ).

Русский

Хвост (tail) (n+1)-кортежа q есть n-кортеж, полученный удалением первого элемента: tail q(i) = q(i.succ).

LaTeX

$$$\forall q: \forall i, \alpha i,\ tail\ q\ i = q\ i.succ$$$

Lean4

/-- The tail of an `n+1` tuple, i.e., its last `n` entries. -/
def tail (q : ∀ i, α i) : ∀ i : Fin n, α i.succ := fun i ↦ q i.succ

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