to₂ — Mathlib

English

A partial function on a product type α × β can be turned into a two-argument partial recursive function.

Русский

Частичную функцию на паре можно превратить в двуарную частичную рекурсивную функцию.

LaTeX

$$$\forall f:\alpha\times\beta\to^.\sigma,\ Partrec(f)\Rightarrow Partrec_2(\lambda a,b. f(a,b)).$$

Lean4

theorem to₂ {f : α × β →. σ} (hf : Partrec f) : Partrec₂ fun a b => f (a, b) :=
  hf.of_eq fun ⟨_, _⟩ => rfl

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