rfindOpt — Mathlib

English

For a function f: α → ℕ → Option σ that is computable, Nat.rfindOpt of f a is partial recursive.

Русский

Для функций f: α → ℕ → Option σ вычислимых, Nat.rfindOpt(f(a)) частично рекурсивна.

LaTeX

$$$\forall f:\alpha\toℕ\to Option\sigma\; (Computable_2(f))\Rightarrow Partrec(\lambda a. Nat.rfindOpt (f(a))).$$

Lean4

theorem rfindOpt {f : α → ℕ → Option σ} (hf : Computable₂ f) : Partrec fun a => Nat.rfindOpt (f a) :=
  (rfind (Primrec.option_isSome.to_comp.comp hf).partrec.to₂).bind (ofOption hf)

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