tail_ofFn — Mathlib

English

The tail of a vector formed by an ofFn function is the vector formed by shifting the function’s input index by one.

Русский

Хвост вектора, созданного через ofFn, — это вектор от функции, с индексами, смещёнными на единицу.

LaTeX

$$$\forall f:\mathrm{Fin}\,n.succ \to \alpha,\; \mathrm{tail}(\mathrm{ofFn}\ f) = \mathrm{ofFn}\ (\lambda i. f(i.succ))$$$

Lean4

@[simp]
theorem tail_ofFn {n : ℕ} (f : Fin n.succ → α) : tail (ofFn f) = ofFn fun i => f i.succ :=
  (ofFn_get _).symm.trans <| by
    congr
    funext i
    rw [get_tail, get_ofFn]
    rfl

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