eq_curry_iff

Mathlib.CategoryTheory.Closed.Cartesian

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

English

Equivalence: curry f = g iff uncurry g = f, in the setting of exponentiable A.

Русский

Эквивалентность: curry f = g ⇔ uncurry g = f.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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