English
A function a ↦ Part.map Option.some (f a) is Partrec iff f is Partrec.
Русский
Функция a ↦ Part.map Some (f a) частично вычислима тогда и только тогда, когда f частично вычислима.
LaTeX
$$$\mathrm{Partrec}\; (\lambda a. \mathrm{Part.map} \mathrm{Option.some} (f a)) \iff \mathrm{Partrec}\; f$$$
Lean4
theorem option_some_iff {f : α →. σ} : (Partrec fun a => (f a).map Option.some) ↔ Partrec f :=
⟨fun h => (Nat.Partrec.ppred.comp h).of_eq fun n => by simp [Part.bind_assoc, bind_some_eq_map], fun hf =>
hf.map (option_some.comp snd).to₂⟩