toList_empty

Mathlib.Data.Vector.Basic

URI: https://scilib.ai/kg/mathlib#List.Vector.toList_empty

English

The underlying list of a length-0 vector is empty.

Русский

Базовый список вектора нулевой длины пуст.

LaTeX

$$$\forall v:\mathrm{Vector}\,\alpha\,0,\; v.toList = []$$$

Lean4

@[simp]
theorem toList_empty (v : Vector α 0) : v.toList = [] :=
  List.length_eq_zero_iff.mp v.2

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru