nat_casesOn — Mathlib

English

Computability of Nat.casesOn is derived from nat_rec by feeding appropriate projections.

Русский

Вычислимость Nat.casesOn получена из nat_rec через соответствующие проекции.

LaTeX

$$$\mathrm{Computable}\;f \land \mathrm{Computable}\; g \land \mathrm{Computable}_2\; h \Rightarrow \mathrm{Computable}\; (a \mapsto \mathrm{Nat}.casesOn (\mathrm{motive}) (f(a)) (g(a)) (h(a)))$$$

Lean4

theorem nat_casesOn {f : α → ℕ} {g : α → σ} {h : α → ℕ → σ} (hf : Computable f) (hg : Computable g)
    (hh : Computable₂ h) : Computable fun a => Nat.casesOn (motive := fun _ => σ) (f a) (g a) (h a) :=
  nat_rec hf hg (hh.comp fst <| fst.comp snd).to₂

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