option_bind₁

Mathlib.Computability.Primrec

URI: https://scilib.ai/kg/mathlib#Primrec.option_bind₁

English

If f : α → Option σ is Primrec, then the function o ↦ Option.bind o f is Primrec.

Русский

Если f : α → Option σ примитивно рекурсивна, то функция o ↦ Option.bind o f является Primrec.

LaTeX

$$$ Primrec f \rightarrow Primrec (\\lambda o. Option.bind o f)$$$

Lean4

theorem option_bind₁ {f : α → Option σ} (hf : Primrec f) : Primrec fun o => Option.bind o f :=
  option_bind .id (hf.comp snd).to₂

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

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

Разделы

Аффилиация

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