English
If o: α → Option β is computable and f,g computable, then the function a ↦ Option.casesOn (o a) (Part.some (f a)) (g a) is computable.
Русский
Если o : α → Option β вычислима, и f,g вычислимы, то a ↦ Option.casesOn (o a) (Some (f a)) (g a) вычислима.
LaTeX
$$$\mathrm{Computable}\; o \to \mathrm{Computable}\; f \to \mathrm{Computable}\; (\mathrm{@Computable}\ _ _ _ (\lambda a. \mathrm{Option}.casesOn (o a) (f a) (g a)))$$$
Lean4
theorem option_casesOn {o : α → Option β} {f : α → σ} {g : α → β → σ} (ho : Computable o) (hf : Computable f)
(hg : Computable₂ g) : @Computable _ σ _ _ fun a => Option.casesOn (o a) (f a) (g a) :=
option_some_iff.1 <|
(nat_casesOn (encode_iff.2 ho) (option_some_iff.2 hf) (map_decode_iff.2 hg)).of_eq fun a => by
cases o a <;> simp [encodek]
