curry — Mathlib

English

For any f: α × β → σ, the curried function Function.curry f is primitive recursive in two variables iff f is primitive recursive.

Русский

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

LaTeX

$$$\operatorname{Primrec}_2(\mathrm{Function.curry} f) \iff \operatorname{Primrec} f$$$

Lean4

theorem curry {f : α × β → σ} : Primrec₂ (Function.curry f) ↔ Primrec f := by rw [← uncurry, Function.uncurry_curry]

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