eq_curry_iff

Mathlib.CategoryTheory.Closed.Monoidal

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

English

Equivalent forms of curry-uncurry as an isomorphism between Hom-sets.

Русский

Эквивалентные формы карри-uncurry как изоморфизм между парами множеств гомоморфизмов.

LaTeX

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

Lean4

theorem eq_curry_iff (f : A ⊗ Y ⟶ X) (g : Y ⟶ A ⟶[C] X) : g = curry f ↔ uncurry g = f :=
  Adjunction.eq_homEquiv_apply (ihom.adjunction A) f g

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

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

Разделы

Аффилиация

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