tail — Mathlib

English

Removing the first element from an injective (n+1)-tuple yields an injective n-tuple obtained by restricting to the tail.

Русский

Извлечение хвоста из инъективной кортежной функции (n+1) элементов даёт инъективную кортежную функцию из n элементов, полученную за счёт хвоста.

LaTeX

$$$\\text{tail}(x) = \\langle \\mathrm{Fin.tail}\,x, x\\text{-injective} \\rangle$$$

Lean4

/-- Remove the first element from an injective (n + 1)-tuple. -/
def tail {n : ℕ} (x : Fin (n + 1) ↪ α) : Fin n ↪ α :=
  ⟨Fin.tail x, x.injective.comp <| Fin.succ_injective _⟩

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