prim_iff₁ — Mathlib

English

A one-argument Primrec' function is primitive recursive, and conversely.

Русский

Функция единичной арности Primrec' эквивалентна Primrec.

LaTeX

$$$\forall {f : \mathbb{N} \to \mathbb{N}},\ (@Primrec'\ 1 \ fun v => f\ v.head) \leftrightarrow \ Primrec\ f$$$

Lean4

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

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