natPair — Mathlib

English

A primitive recursive expression for the Cantor pairing of two naturals is Primrec'.

Русский

Парочка Натуральных чисел через пару Кантора является Primrec'.

LaTeX

$$$\mathrm{natPair} : \ Primrec'\ 2\ (fun v => Nat.pair v.head v.tail.head)$$$

Lean4

theorem natPair : @Primrec' 2 fun v => v.head.pair v.tail.head :=
  if_lt head (tail head) (add.comp₂ _ (tail <| mul.comp₂ _ head head) head)
    (add.comp₂ _ (add.comp₂ _ (mul.comp₂ _ head head) head) (tail head))

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