not

Mathlib.Computability.Primrec

URI: https://scilib.ai/kg/mathlib#PrimrecRel.not

English

If R is decidable, then the relation (L,b) ↦ ∃ a ∈ L, R(a,b) is primitive recursive.

Русский

Если R разрешимо, то отношение (L,b) ↦ ∃ a ∈ L, R(a,b) является примитивно-рекурсивным.

LaTeX

$$$\mathrm{PR}\big( (L,b) \mapsto \exists a \in L\, R(a,b) \big).$$$

Lean4

protected theorem not (hf : PrimrecRel R) : PrimrecRel fun a b ↦ ¬R a b :=
  PrimrecPred.not hf

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

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

Разделы

Аффилиация

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