option_some_iff — Mathlib

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₂⟩

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