computablePred_iff_computable_decide

English

A predicate p is computable if and only if there exists a computable function f such that p(a) holds exactly when f(a) equals true.

Русский

Предикат p вычислим, если и только если существует вычислимая функция f, такая что p(a) выполняется тогда и только тогда, когда f(a) равно true.

LaTeX

$$ComputablePred p ↔ Computable (fun a => decide (p a))$$

Lean4

theorem computablePred_iff_computable_decide {p : α → Prop} [DecidablePred p] :
    ComputablePred p ↔ Computable (fun a => decide (p a))
    where
  mp := ComputablePred.decide
  mpr := Computable.computablePred

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