head?_toList

Mathlib.Data.Vector.Basic

URI: https://scilib.ai/kg/mathlib#List.Vector.head?_toList

English

The optional head of toList corresponds to the actual head of the vector.

Русский

Опциональное значение head? списка toList соответствует голове вектора.

LaTeX

$$$\forall v:\mathrm{Vector}\,\alpha\,n.succ,\; (\mathrm{toList}\ v).head? = \mathrm{some}(\mathrm{head}\ v)$$$

Lean4

theorem head?_toList : ∀ v : Vector α n.succ, (toList v).head? = some (head v)
  | ⟨_ :: _, _⟩ => rfl

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

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

Разделы

Аффилиация

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