option_some_iff — Mathlib

English

A function a ↦ Option.some(f(a)) is computable iff f is computable (given codability assumptions).

Русский

Функция a ↦ Option.some(f(a)) вычислима тогда и только тогда, когда f вычислима (при выполнении допущений о кодируемости).

LaTeX

$$$(\text{Computablefun } a \mapsto \mathrm{Option}.some(f(a))) \iff \mathrm{Computable} f$$$

Lean4

theorem option_some_iff {f : α → σ} : (Computable fun a => Option.some (f a)) ↔ Computable f :=
  ⟨fun h => encode_iff.1 <| Primrec.pred.to_comp.comp <| encode_iff.2 h, option_some.comp⟩

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