append_def — Mathlib

English

The concatenation operation on vectors is equivalent to pattern matching on the two input vectors and producing the concatenation of their underlying lists.

Русский

Объединение векторов эквивалентно разбивке по входным векторам и построению конкатенации их списков.

LaTeX

$$$(\\text{HAppend.hAppend} : Vector \\alpha n \\to Vector \\alpha m \\to Vector \\alpha (n+m)) = \\text{fun }\\langle x_1,h_1\\rangle, \\langle x_2,h_2\\rangle => \\langle x_1 ++ x_2, \\ldots \\rangle$$$

Lean4

theorem append_def {n m : Nat} :
    (HAppend.hAppend : Vector α n → Vector α m → Vector α (n + m)) = fun
      | ⟨l₁, h₁⟩, ⟨l₂, h₂⟩ => ⟨l₁ ++ l₂, by simp [*]⟩ :=
  rfl

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