tail_def — Mathlib

English

For a family q : ∀ i, α i, the tail of the tuple is exactly the shift: tail (λ k, q k) = λ k, q k.succ.

Русский

Для family q: ∀ i, α i хвост кортежа совпадает со сдвигом: tail(λk, q k) = λk, q k.succ.

LaTeX

$$$\text{tail} (\lambda k. q k) = \lambda k. q k.succ$$$

Lean4

theorem tail_def {n : ℕ} {α : Fin (n + 1) → Sort*} {q : ∀ i, α i} :
    (tail fun k : Fin (n + 1) ↦ q k) = fun k : Fin n ↦ q k.succ :=
  rfl

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