option_map — Mathlib

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

Похожие утверждения