toList_append — Mathlib

English

Appending vectors corresponds under toList to appending lists: toList (v ++ w) = toList v ++ toList w.

Русский

Сложение векторов соответствует сложению списков под toList: toList (v ++ w) = toList v ++ toList w.

LaTeX

$$@[simp]\\ntheorem toList_append {n m : \\mathbb{N}} (v : Vector α n) (w : Vector α m) : toList (v ++ w) = toList v ++ toList w$$

Lean4

/-- Appending of vectors corresponds under `toList` to appending of lists. -/
@[simp]
theorem toList_append {n m : ℕ} (v : Vector α n) (w : Vector α m) : toList (v ++ w) = toList v ++ toList w :=
  rfl

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