primrec₂_pair — Mathlib

English

The two-argument constructor pair is primitive recursive.

Русский

Конструктор с двумя входами, пара, является примитивно рекурсивным.

LaTeX

$$$\\operatorname{Primrec}_2(\\text{pair})$$$

Lean4

theorem primrec₂_pair : Primrec₂ pair :=
  Primrec₂.ofNat_iff.2 <|
    Primrec₂.encode_iff.1 <|
      nat_add.comp
        (nat_double.comp <|
          nat_double.comp <|
            Primrec₂.natPair.comp (encode_iff.2 <| (Primrec.ofNat Code).comp fst)
              (encode_iff.2 <| (Primrec.ofNat Code).comp snd))
        (Primrec₂.const 4)

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