encdec — Mathlib

English

For any α with a Primcodable structure, the map n ↦ encode (decode α n) is primitive recursive.

Русский

Для любого α с примкодируемой структурой отображение n ↦ encode (decode α n) является примитивно-рекурсивным.

LaTeX

$$$$ \\mathrm{Primrec}\\left(\\lambda n. \\mathrm{encode}(\\mathrm{decode}_{\\alpha}(n))\\right) $$.$$

Lean4

theorem encdec : Primrec fun n => encode (@decode α _ n) :=
  nat_iff.2 (Primcodable.prim _)

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