option_map₁

Mathlib.Computability.Primrec

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

English

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

Русский

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

LaTeX

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

Lean4

theorem option_map₁ {f : α → σ} (hf : Primrec f) : Primrec (Option.map f) :=
  option_map .id (hf.comp snd).to₂

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

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

Разделы

Аффилиация

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