head_cons_tail

Mathlib.Data.List.Basic

URI: https://scilib.ai/kg/mathlib#List.head_cons_tail

English

For any nonempty list x, x equals head h of x concatenated with tail x, i.e., x = head h :: tail x.

Русский

Для любого непустого списка x выполняется x = head h :: tail x.

LaTeX

$$$\\\\forall x \\\\; (\\\\exists h, x = \\\\mathrm{head} \\\\; h \\\\; \\\\mathrm{tail} \\\\; x)$$$

Lean4

@[deprecated cons_head_tail (since := "2025-08-15")]
theorem head_cons_tail (x : List α) (h : x ≠ []) : x.head h :: x.tail = x := by simp

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

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

Разделы

Аффилиация

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