head_eq_some

Mathlib.Data.Seq.Defs

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

← MathLib Explorer

English

If s.head = some x, then s = cons x s.tail.

Русский

Если s.head = some x, тогда s = cons x s.tail.

LaTeX

$$$\\forall {s:\\mathrm{Seq}\\alpha} {x:\\alpha},\\; \\mathrm{head}\\ s = \\mathrm{some}\\ x \\Rightarrow s = \\mathrm{cons}\\ x\\ s.tail$$$

Lean4

theorem head_eq_some {s : Seq α} {x : α} (h : s.head = some x) : s = cons x s.tail :=
  by
  ext1 n
  cases n <;> simp only [get?_cons_zero, get?_cons_succ, get?_tail]
  exact h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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