get?_cons_zero

Mathlib.Data.Seq.Defs

URI: https://scilib.ai/kg/mathlib#Stream'.Seq.get?_cons_zero

English

@[simp] get? on the constructed sequence from f and hf returns f.

Русский

Для сконструированной последовательности из f и hf get? возвращает f.

LaTeX

$$$@[simp] \\; \\operatorname{get?} \\; (\\langle f, hf\\rangle) = f$$$

Lean4

@[simp]
theorem get?_cons_zero (a : α) (s : Seq α) : (cons a s).get? 0 = some a :=
  rfl

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

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

Разделы

Аффилиация

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