English
Let v be a vector of length m. Then taking the first n coordinates and converting to a list yields the same result as taking the first n elements from the list obtained from v.
Русский
Пусть v — вектор длины m. Тогда взятие первых n координат и преобразование в список дают тот же результат, что и взятие первых n элементов у списка, полученного из v.
LaTeX
$$$\operatorname{toList}(\operatorname{take} n\, v) = \operatorname{List.take} n (\operatorname{toList} v)$$$
Lean4
/-- `take` of vectors corresponds under `toList` to `take` of lists. -/
@[simp]
theorem toList_take {n m : ℕ} (v : Vector α m) : toList (take n v) = List.take n (toList v) :=
by
cases v
rfl
