tail — Mathlib

English

Define tail on Fin(n+1) →₀ M by discarding the first coordinate and reindexing the rest; it maps Fin(n+1) family to Fin n family.

Русский

Определим tail на Fin(n+1) →₀ M, который отбрасывает первый координат и переносит остальные индексы к Fin n.

LaTeX

$$$\\mathrm{tail} : \\mathrm{Fin} (n+1) \\to_0 M \\to \\mathrm{Fin} n \\to_0 M$$$

Lean4

/-- `tail` for maps `Fin (n + 1) →₀ M`. See `Fin.tail` for more details. -/
def tail (s : Fin (n + 1) →₀ M) : Fin n →₀ M :=
  Finsupp.equivFunOnFinite.symm (Fin.tail s)

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