option_getD — Mathlib

English

Given computable f: α → Option β and computable g: α → β, the function a ↦ (f a).getD (g a) is computable.

Русский

Для вычислимых f: α → Option β и g: α → β функция a ↦ (f a).getD (g a) вычислима.

LaTeX

$$$\mathrm{Computable}\; f \to \mathrm{Computable}\; g \Rightarrow \mathrm{Computable}\; (a \mapsto (f a).\mathrm{getD}(g a))$$$

Lean4

theorem option_getD {f : α → Option β} {g : α → β} (hf : Computable f) (hg : Computable g) :
    Computable fun a => (f a).getD (g a) :=
  (Computable.option_casesOn hf hg (show Computable₂ fun _ b => b from Computable.snd)).of_eq fun a => by
    cases f a <;> rfl

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