nat_iff — Mathlib

English

Let f: N → N. Then f is Primrec if and only if f belongs to the standard class of natural-primitive-recursive functions, i.e. Nat.Primrec f.

Русский

Пусть f: ℕ → ℕ. Тогда f является примитивно-рекурсивной тогда и только тогда, когда f принадлежит стандартному классу примитивно-рекурсивных функций Nat.Primrec f.

LaTeX

$$$$ \\mathrm{Primrec}(f) \\iff \\mathrm{Nat.Primrec}(f) $$$$

Lean4

theorem nat_iff {f : ℕ → ℕ} : Primrec f ↔ Nat.Primrec f :=
  dom_denumerable

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