not_empty_toList

Mathlib.Data.Vector.Basic

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

English

As above, the toList of a nontrivial vector is nonempty.

Русский

Как выше, список toList непуст для непустого вектора.

LaTeX

$$$\forall v:\mathrm{Vector}\,\alpha\,(\mathrm{succ}\;n),\; \neg(v.toList = [])$$$

Lean4

theorem not_empty_toList (v : Vector α (n + 1)) : ¬v.toList.isEmpty := by
  simp only [empty_toList_eq_ff, Bool.coe_sort_false, not_false_iff]

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

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

Разделы

Аффилиация

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