English
If f : α → Option β and g : α → β → σ are computable, then a ↦ (f a).map (g a) is computable.
Русский
Если f : α → Option β и g : α → β → σ вычислимы, то a ↦ (f a).map (g a) вычислимо.
LaTeX
$$$\mathrm{Computable}\; f \to \mathrm{Computable}_2\; g \Rightarrow \mathrm{Computable}\; (a \mapsto (f(a)).\mathrm{map}\; (g(a)))$$$
Lean4
theorem option_map {f : α → Option β} {g : α → β → σ} (hf : Computable f) (hg : Computable₂ g) :
Computable fun a => (f a).map (g a) :=
by
convert option_bind hf (option_some.comp₂ hg)
apply Option.map_eq_bind