comp — Mathlib

English

Given computable f and g and a Partrec₂ h, one can form a partial recursion that performs Nat.casesOn on f(a) with given branches.

Русский

Имея вычислимые f и g и Partrec₂ h можно получить частично рекурсивную функцию, выполняющую Nat.casesOn над f(a) с заданными ветвями.

LaTeX

$$$\forall f,g,h,\Computable(f) \land \Computable(g) \land \Partrec_2(h) \Rightarrow\Partrec(\lambda a. Nat.casesOn (f(a)) (Part.some (g(a))) (h(a))).$$

Lean4

nonrec theorem comp {f : β → γ → σ} {g : α → β} {h : α → γ} (hf : Computable₂ f) (hg : Computable g)
    (hh : Computable h) : Computable fun a => f (g a) (h a) :=
  hf.comp (hg.pair hh)

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