get?_mk

Mathlib.Data.Seq.Defs

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

English

For any f with hf, the nth element of the constructed sequence ⟨f, hf⟩ is exactly f.

Русский

Для любого f с hf, элемент последовательности, построенной как ⟨f, hf⟩, равен f.

LaTeX

$$$\\forall f:\\mathbb{N}\\to \\mathrm{Option}\\,\\alpha\\,\\, hf,\\; \\operatorname{get?}(\\langle f, hf\\rangle) = f.$$$

Lean4

@[simp]
theorem get?_mk (f hf) : @get? α ⟨f, hf⟩ = f :=
  rfl

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

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

Разделы

Аффилиация

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