append — Mathlib

English

Append two vectors: the resulting vector has length m+n and is defined by recursion on the first argument: append(v,w) = v.recOn(w, (a,_ ,IH) => a :: IH).

Русский

Объединение двух векторов: полученный вектор имеет длину m+n и определяется по рекурсии по первому аргументу: append(v,w) = v.recOn(w, (a,_,IH) => a :: IH).

LaTeX

$$$ \mathrm{append}(v,w) = v.\mathrm{recOn}\, w\; (\lambda a, \_ , IH.\; a :: IH). $$$

Lean4

/-- Append two vectors -/
def append (v : Vector3 α m) (w : Vector3 α n) : Vector3 α (n + m) :=
  v.recOn w (fun a _ IH => a :: IH)

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