cons — Mathlib

English

Adding an element at the beginning of an (n)-tuple, to obtain an (n+1)-tuple, is given by cons x p: Fin (n+1) → α i = Fin.cases x p i.

Русский

Добавление элемента в начало (n)-кортежа для получения (n+1)-кортежа задаётся как cons x p: Fin(n+1) → α i = Fin.cases x p i.

LaTeX

$$$\text{cons}\ (x)\ (p)\ i = \mathrm{Fin.cases}(x,p)(i)$$$

Lean4

/-- Adding an element at the beginning of an `n`-tuple, to get an `n+1`-tuple. -/
def cons (x : α 0) (p : ∀ i : Fin n, α i.succ) : ∀ i, α i := fun j ↦ Fin.cases x p j

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