uncurry — Mathlib

English

For any f: α → β → σ, the uncurried function on α × β, given by uncurry f, is primitive recursive iff f is primitive recursive in two arguments.

Русский

Для любой f: α → β → σ, функция uncurry f на α × β является примитивно вычислимой тогда и только тогда, когда f является примитивно вычислимой по двум аргументам.

LaTeX

$$$\bigl(\operatorname{Primrec}(\mathrm{Function.uncurry} f)\bigr) \iff \operatorname{Primrec}_2 f$$$

Lean4

theorem uncurry {f : α → β → σ} : Primrec (Function.uncurry f) ↔ Primrec₂ f := by
  rw [show Function.uncurry f = fun p : α × β => f p.1 p.2 from funext fun ⟨a, b⟩ => rfl]; rfl

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