English
If f : α → β ⊕ γ and g,h computable with h: α → γ →. σ, then a ↦ Sum.casesOn (f a) (λ b. Some (g a b)) (h a) is computable.
Русский
Если f : α → β ⊕ γ, g: α → β → σ и h: α → γ →. σ вычислимы, то a ↦ Sum.casesOn (f a) (λ b. Some (g a b)) (h a) вычислима.
LaTeX
$$$\mathrm{Computable}\; f \to \mathrm{Computable}_2\; g \to \mathrm{Computable}_2\; h \Rightarrow \mathrm{Computable}\; (a \mapsto \mathrm{Sum}.casesOn (f a) (\lambda b. \mathrm{Some}(g a b)) (h a))$$$
Lean4
theorem sumCasesOn_right {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ →. σ} (hf : Computable f) (hg : Computable₂ g)
(hh : Partrec₂ h) : @Partrec _ σ _ _ fun a => Sum.casesOn (f a) (fun b => Part.some (g a b)) (h a) :=
have :
Partrec fun a =>
(Option.casesOn (Sum.casesOn (f a) (fun _ => Option.none) Option.some : Option γ)
(some (Sum.casesOn (f a) (fun b => some (g a b)) fun _ => Option.none)) fun c => (h a c).map Option.some :
Part (Option σ)) :=
optionCasesOn_right (g := fun a n => Part.map Option.some (h a n))
(sumCasesOn hf (const Option.none).to₂ (option_some.comp snd).to₂)
(sumCasesOn (g := fun a n => Option.some (g a n)) hf (option_some.comp hg) (const Option.none).to₂)
(option_some_iff.2 hh)
option_some_iff.1 <| this.of_eq fun a => by cases f a <;> simp
