nat_iff — Mathlib

English

Encoding/decoding preserves partial recursiveness: Partrec of the map-encoded function is equivalent to Partrec of the original function.

Русский

Кодирование/декодирование сохраняют частичную рекурсивность: Partrec для отображения кодирования эквивалентна Partrec исходной функции.

LaTeX

$$$\forall f:\alpha\to^.\sigma,\ Partrec(\lambda a. Part.map encode (f a)) \iff Partrec(f).$$

Lean4

theorem nat_iff {f : ℕ →. ℕ} : Partrec f ↔ Nat.Partrec f := by simp [Partrec, map_id']

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