curry_eq

Mathlib.CategoryTheory.Closed.Cartesian

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CartesianClosed.curry_eq

English

In a cartesian closed category with exponentiable A, for f and g, curry f = g iff uncurry g = f.

Русский

В категории, замкнутой по декартову произведению, при экспоненциируемом A, curry f = g ⇔ uncurry g = f.

LaTeX

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

Lean4

theorem curry_eq (g : A ⊗ Y ⟶ X) : curry g = (exp.coev A).app Y ≫ (exp A).map g :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru