part_iff₁ — Mathlib

English

Let f be a unary function f: N → N. Then f is Partrec iff the corresponding one-argument vector encoding is Partrec'.

Русский

Пусть f: ℕ → ℕ. Тогда f частично рекурсиво, если и только если соответствующая одарная запись через Partrec' для одной переменной тоже частично рекурсива.

LaTeX

$$$ \forall f: \mathbb{N} \to \mathbb{N},\; _root_.Partrec f \iff @Partrec' 1 (\lambda v. f(v.head)) $$$

Lean4

theorem part_iff₁ {f : ℕ →. ℕ} : (@Partrec' 1 fun v => f v.head) ↔ _root_.Partrec f :=
  part_iff.trans
    ⟨fun h =>
      (h.comp <| (Primrec.vector_ofFn fun _ => _root_.Primrec.id).to_comp).of_eq fun v => by simp only [id, head_ofFn],
      fun h => h.comp vector_head⟩

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