English
If f : α → β ⊕ γ is computable and g,h are computable, then a ↦ Sum.casesOn (f a) (g a) (h a) is computable.
Русский
Если f : α → β ⊕ γ вычислима, а g и h вычислимы, то a ↦ Sum.casesOn (f a) (g a) (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) (g a) (h a))$$$
Lean4
theorem sumCasesOn {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ → σ} (hf : Computable f) (hg : Computable₂ g)
(hh : Computable₂ h) : @Computable _ σ _ _ fun a => Sum.casesOn (f a) (g a) (h a) :=
option_some_iff.1 <|
(cond (nat_bodd.comp <| encode_iff.2 hf)
(option_map (Computable.decode.comp <| nat_div2.comp <| encode_iff.2 hf) hh)
(option_map (Computable.decode.comp <| nat_div2.comp <| encode_iff.2 hf) hg)).of_eq
fun a => by rcases f a with b | c <;> simp [Nat.div2_val]
