encode_iff — Mathlib

English

For any f, the function n ↦ encode (f(n)) is primitive recursive if and only if f is primitive recursive.

Русский

Для любой f функция n ↦ encode (f(n)) примрrec тогда и только тогда, когда f примрrec.

LaTeX

$$$$ (\\mathrm{Primrec}\\bigl(\\lambda a. \\mathrm{encode}(f(a))\\bigr)) \\iff \\mathrm{Primrec}(f) $$$$

Lean4

theorem encode_iff {f : α → σ} : (Primrec fun a => encode (f a)) ↔ Primrec f :=
  ⟨fun h => Nat.Primrec.of_eq h fun n => by cases @decode α _ n <;> rfl, Primrec.encode.comp⟩

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