head_cons

Mathlib.Data.Seq.Defs

URI: https://scilib.ai/kg/mathlib#Stream'.Seq.head_cons

English

head (cons a s) = some a.

Русский

head (cons a s) = some a.

LaTeX

$$$\\mathrm{head}(\\mathrm{cons}\\ a\\ s) = \\mathrm{some}\\ a$$$

Lean4

@[simp]
theorem head_cons (a : α) (s) : head (cons a s) = some a := by
  rw [head_eq_destruct, destruct_cons, Option.map_eq_map, Option.map_some]

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

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

Разделы

Аффилиация

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