decide — Mathlib

English

If p is a decidable predicate and hp is a computable predicate for p, then there exists a computable predicate for p that returns a Boolean value representing p.

Русский

Если p — распознаваемое по определению свойство, и hp — вычислимое свойство p, то существует вычислимое свойство p, возвращающее булево значение, означающее p.

LaTeX

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

Lean4

protected theorem decide {p : α → Prop} [DecidablePred p] (hp : ComputablePred p) :
    Computable (fun a => decide (p a)) := by convert hp.choose_spec

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