head_mem

Mathlib.Data.Vector.Mem

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

English

The head of a vector of length n+1 belongs to its toList.

Русский

Голова вектора длиной n+1 принадлежит его toList.

LaTeX

$$$$ v.head \in v.toList $$$$

Lean4

@[simp]
theorem head_mem (v : Vector α (n + 1)) : v.head ∈ v.toList :=
  (Vector.mem_iff_get v.head v).2 ⟨0, Vector.get_zero v⟩

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

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

Разделы

Аффилиация

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