curry_eq_iff — Mathlib

English

Between A ⊗ Y and X, g = curry f if and only if uncurry g = f, i.e., the curry/uncurry correspondence is bijective.

Русский

Для отображений между A ⊗ Y и X равенство g = curry f эквивалентно uncurry g = f.

LaTeX

$$$g = \mathrm{curry} f \iff \mathrm{uncurry} g = f$$$

Lean4

theorem curry_eq_iff (f : A ⊗ Y ⟶ X) (g : Y ⟶ A ⟹ X) : curry f = g ↔ f = uncurry g :=
  Adjunction.homEquiv_apply_eq (exp.adjunction A) f g

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