natPair — Mathlib

English

The Nat.pair function, sending a pair of natural numbers to a single natural number, is primitive recursive in two arguments.

Русский

Функция Nat.pair, объединяющая пару натуральных чисел в одно число, является примитивно вычислимой функцией двумя аргументами.

LaTeX

$$$\operatorname{Primrec}_2(\mathrm{Nat.pair})$$$

Lean4

theorem natPair : Primrec₂ Nat.pair := by simp [Primrec₂, Primrec]; constructor

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