ofOption — Mathlib

English

If f is computable, then a ↦ (f a) as a partial is Partrec.

Русский

Если f вычислима, то a ↦ (f a) как частично заданная функция — Partrec.

LaTeX

$$$\text{Computable } f \Rightarrow \text{Partrec } (\lambda a. (f a : \mathrm{Part} \beta))$$$

Lean4

theorem ofOption {f : α → Option β} (hf : Computable f) : Partrec fun a => (f a : Part β) :=
  (Nat.Partrec.ppred.comp hf).of_eq fun n =>
    by
    rcases decode (α := α) n with - | a <;> simp
    rcases f a with - | b <;> simp

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