cons_head!_tail

Mathlib.Data.List.Basic

URI: https://scilib.ai/kg/mathlib#List.cons_head!_tail

English

If l ≠ ∅, then head! l :: tail l = l.

Русский

Если список не пуст, то head! l :: tail l = l.

LaTeX

$$$\\\\mathrm{head!}\ a \\\\;\\\\; tail\full l = l$$$

Lean4

theorem cons_head!_tail [Inhabited α] {l : List α} (h : l ≠ []) : head! l :: tail l = l :=
  cons_head?_tail (head!_mem_head? h)

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

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

Разделы

Аффилиация

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