left

Mathlib.Computability.Primrec

URI: https://scilib.ai/kg/mathlib#Primrec₂.left

English

The first projection map (a, b) ↦ a from α × β to α is primitive recursive in two variables.

Русский

Первая проекция (a, b) ↦ a из α × β в α является примитивно вычислимой функцией двумя переменными.

LaTeX

$$$\operatorname{Primrec}_2(\mathrm{fst})$$$

Lean4

theorem left : Primrec₂ fun (a : α) (_ : β) => a :=
  .fst

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

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

Разделы

Аффилиация

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