computablePred

Mathlib.Computability.Halting

URI: https://scilib.ai/kg/mathlib#Computable.computablePred

English

See ComputablePred.decide; the lemma provides a decision procedure for a decidable predicate.

Русский

См. ComputablePred.decide; даёт процедуру решения для распознаваемого предиката.

LaTeX

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

Lean4

theorem computablePred {p : α → Prop} [DecidablePred p] (hp : Computable (fun a => decide (p a))) : ComputablePred p :=
  ⟨inferInstance, hp⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru