empty_toList_eq_ff

Mathlib.Data.Vector.Basic

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

English

For any vector of length n+1, its toList is nonempty.

Русский

Для любого вектора длины n+1 список toList непуст.

LaTeX

$$$\forall\alpha\; \forall n\; (v:\mathrm{Vector}\,\alpha\,(n+1)),\ v.toList.\mathrm{isEmpty} = \mathrm{false}$$$

Lean4

@[simp]
theorem empty_toList_eq_ff (v : Vector α (n + 1)) : v.toList.isEmpty = false :=
  match v with
  | ⟨_ :: _, _⟩ => rfl

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

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

Разделы

Аффилиация

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