pair — Mathlib

English

Let α and β be types with primitive encodings. The pairing map (a, b) ↦ (a, b) from α × β to α × β is primitive recursive in two arguments.

Русский

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

LaTeX

$$$\operatorname{Primrec}_2(\mathrm{Prod.mk})$$$

Lean4

protected theorem pair : Primrec₂ (@Prod.mk α β) :=
  Primrec.pair .fst .snd

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