nat_rec₁

Mathlib.Computability.Primrec

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

English

For any a and Primrec₂ f, the function n ↦ Nat.rec a f n is Primrec.

Русский

Для любого a и Primrec₂ f функция n ↦ Nat.rec a f n является Primrec.

LaTeX

$$$ Primrec_2 f \rightarrow Primrec (\\lambda n. Nat.rec a f n)$$$

Lean4

theorem nat_rec₁ {f : ℕ → α → α} (a : α) (hf : Primrec₂ f) : Primrec (Nat.rec a f) :=
  nat_rec' .id (const a) <| comp₂ hf Primrec₂.right

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

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

Разделы

Аффилиация

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