vecCons — Mathlib

English

vecCons prepends an entry h to a vector t, i.e., vecCons h t = Fin.cons h t.

Русский

vecCons добавляет в начало вектора t элемент h: vecCons h t = Fin.cons h t.

LaTeX

$$$\\operatorname{vecCons} \\{n:\\mathbb{N}\\} (h:\\alpha) (t:\\mathrm{Fin} n \\to \\alpha) : \\mathrm{Fin}(n.succ) \\to \\alpha = \\mathrm{Fin}.cons h t$$$

Lean4

/-- `vecCons h t` prepends an entry `h` to a vector `t`.

The inverse functions are `vecHead` and `vecTail`.
The notation `![a, b, ...]` expands to `vecCons a (vecCons b ...)`.
-/
def vecCons {n : ℕ} (h : α) (t : Fin n → α) : Fin n.succ → α :=
  Fin.cons h t

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