English
If f: α → β and g: α → γ are primitive recursive, then a ↦ (f(a), g(a)) is primitive recursive.
Русский
Если f: α → β и g: α → γ примрrec, то a ↦ (f(a), g(a)) примрrec.
LaTeX
$$$$ \\forall f:\\alpha\\to\\beta,\\; \\forall g:\\alpha\\to\\gamma,\\ \\mathrm{Primrec}(f) \\to \\mathrm{Primrec}(g) \\to \\mathrm{Primrec}(\\lambda a. (f(a), g(a))) $$$$
Lean4
theorem pair {α β γ} [Primcodable α] [Primcodable β] [Primcodable γ] {f : α → β} {g : α → γ} (hf : Primrec f)
(hg : Primrec g) : Primrec fun a => (f a, g a) :=
((casesOn1 0 (Nat.Primrec.succ.comp <| .pair (Nat.Primrec.pred.comp hf) (Nat.Primrec.pred.comp hg))).comp
(Primcodable.prim α)).of_eq
fun n => by cases @decode α _ n <;> simp [encodek]
