partrec₂ — Mathlib

English

If f is Computable₂, then the curried version a ↦ (f a) is Partrec₂.

Русский

Если f вычислимая двухаргументная функция, то карардированная версия является Partrec₂.

LaTeX

$$$\text{Computable₂ } f \Rightarrow \text{Partrec₂ } (\lambda a. f(a))$$$

Lean4

protected theorem partrec₂ {α β σ} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α → β → σ}
    (hf : Computable₂ f) : Partrec₂ fun a => (f a : β →. σ) :=
  hf

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