encode_iff — Mathlib

English

For any f: α → β → σ with primcodable α, β, σ, encoding the outputs of f preserves primitive recursiveness: Primrec₂ (a,b) ↦ encode(f(a,b)) iff Primrec₂ f.

Русский

Для любых f: α → β → σ с примитивно кодируемыми α, β, σ сохранение кодирования выходов f сохраняет примитивную рекурсию: Primrec₂ (a,b) ↦ encode(f(a,b)) эквивалентно Primrec₂ f.

LaTeX

$$$\bigl(\operatorname{Primrec}_2\, (\lambda a,b. \operatorname{encode}(f(a,b)))\bigr) \iff \operatorname{Primrec}_2 f$$$

Lean4

theorem encode_iff {f : α → β → σ} : (Primrec₂ fun a b => encode (f a b)) ↔ Primrec₂ f :=
  Primrec.encode_iff

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