insert — Mathlib

English

Insert a into v at index i ∈ Fin2(n+1) to obtain a vector of length n+1: insert(a,v,i) is the vector (a :: v) composed with insertPerm i.

Русский

Вставить элемент a в вектор v на позиции i ∈ Fin2(n+1) даёт вектор длины n+1: insert(a,v,i) = (a :: v) ∘ insertPerm i.

LaTeX

$$$ \mathrm{insert}(a,v,i) = (a :: v) \circ \mathrm{insertPerm}(i). $$$

Lean4

/-- Insert `a` into `v` at index `i`. -/
def insert (a : α) (v : Vector3 α n) (i : Fin2 (n + 1)) : Vector3 α (n + 1) := fun j => (a :: v) (insertPerm i j)

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