of_eq_tot — Mathlib

English

If f is partial recursive and for all inputs n, g(n) lies in the value f(n), then g is computable.

Русский

Если f частично рекурсивна и для каждого входа n значение g(n) принадлежит f(n), то g вычислима.

LaTeX

$$$\forall \alpha\sigma\,[\text{Primcodable }\alpha]\,[\text{Primcodable }\sigma]\;\forall f:\alpha\to^.\sigma\,\forall g:\alpha\to\sigma:\ Partrec(f) \to (\forall n:\alpha, g(n)\in f(n)) \to Computable(g).$$

Lean4

theorem of_eq_tot {f : α →. σ} {g : α → σ} (hf : Partrec f) (H : ∀ n, g n ∈ f n) : Computable g :=
  hf.of_eq fun a => eq_some_iff.2 (H a)

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