init — Mathlib

English

The beginning of an (n+1)-tuple is obtained by taking the first n entries, i.e., init q i.castSucc = q i.castSucc for i ∈ Fin n.

Русский

Начало (n+1)-кортежа получается из первых n элементов: init q i.castSucc = q i.castSucc для i ∈ Fin n.

LaTeX

$$$\\mathrm{Fin.init}\\ q\\ i = q\\ i.castSucc$$$

Lean4

/-- The beginning of an `n+1` tuple, i.e., its first `n` entries -/
def init (q : ∀ i, α i) (i : Fin n) : α i.castSucc :=
  q i.castSucc

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