computablePred

Mathlib.Computability.Halting

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

English

If p is a PrimrecPred predicate, then p is computable in the sense of ComputablePred.

Русский

Если p является примрековым предикатом, то он вычислим в смысле ComputablePred.

LaTeX

$$PrimrecPred p → ComputablePred p$$

Lean4

theorem computablePred {α} [Primcodable α] {p : α → Prop} : (hp : PrimrecPred p) → ComputablePred p
  | ⟨_, hp⟩ => hp.to_comp.computablePred

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

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

Разделы

Аффилиация

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