head_eq_destruct

Mathlib.Data.Seq.Defs

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

English

head s equals the first component of destruct s.

Русский

head s равен первой компоненте destruct s.

LaTeX

$$$\\mathrm{head}\\;s = \\mathrm{Prod.fst}\\,\\langle \\mathrm{destruct}\\;s \\rangle.$$$

Lean4

theorem head_eq_destruct (s : Seq α) : head s = Prod.fst <$> destruct.{u} s := by unfold destruct head;
  cases get? s 0 <;> rfl

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

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

Разделы

Аффилиация

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