English
If f is computable and g,h computable with g producing functions, then a ↦ Sum.casesOn (f a) (g a) (λ c, Some (h a c)) is computable.
Русский
Если f вычислима, а g,h вычислимы с выводом функций, то a ↦ Sum.casesOn (f a) (g a) (λ c, Some (h a c)) вычислима.
LaTeX
$$$\mathrm{Computable}\; f \to \mathrm{Computable}_2\; g \to \mathrm{Computable}_2\; h \Rightarrow \mathrm{Computable}\; (a \mapsto \mathrm{Sum}.casesOn (f a) (g a) (\lambda c. \mathrm{Some}(h a c)))$$$
Lean4
theorem sumCasesOn_left {f : α → β ⊕ γ} {g : α → β →. σ} {h : α → γ → σ} (hf : Computable f) (hg : Partrec₂ g)
(hh : Computable₂ h) : @Partrec _ σ _ _ fun a => Sum.casesOn (f a) (g a) fun c => Part.some (h a c) :=
(sumCasesOn_right (sumCasesOn hf (sumInr.comp snd).to₂ (sumInl.comp snd).to₂) hh hg).of_eq fun a => by
cases f a <;> simp
