primrecRel

Mathlib.Computability.Primrec

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

English

If p is a PrimrecPred on α × β, then the relation a,b ↦ p (a,b) is a PrimrecRel.

Русский

Если p — PrimrecPred на α × β, то отношение a,b ↦ p (a,b) является PrimrecRel.

LaTeX

$$$ PrimrecPred p \rightarrow PrimrecRel (\\lambda a b. p (a,b))$$$

Lean4

theorem _root_.PrimrecPred.primrecRel {p : α × β → Prop} (hp : PrimrecPred p) : PrimrecRel fun a b => p (a, b) :=
  hp

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

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

Разделы

Аффилиация

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