partrec_iff_forall_turingReducible

English

A function is partial recursive iff it is recursive in every partial function g.

Русский

Частная функция является частично рекурсивной тогда и только тогда, когда она рекурсивна во всех частичных функциях g.

LaTeX

$$$ \text{Nat.Partrec } f \iff \forall g, f \le_T g $$$

Lean4

/-- A partial function `f` is partial recursive if and only if it is recursive in
every partial function `g`.
-/
theorem partrec_iff_forall_turingReducible : Nat.Partrec f ↔ ∀ g, f ≤ᵀ g :=
  ⟨fun hf _ ↦ hf.turingReducible, (· _ |>.partrec_of_zero)⟩

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