enrichedOrdinaryCategorySelf_homEquiv

Mathlib.CategoryTheory.Closed.Enrichment

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

English

The symmetric statement: the inverse of eHomEquiv corresponds to uncurry'.

Русский

Симметрически: обратное отображение eHomEquiv соответствует uncurry'.

LaTeX

$$$ (eHomEquiv\; C)\;{}.\mathrm{symm}\; g = \mathrm{uncurry'}\; g $$$

Lean4

theorem enrichedOrdinaryCategorySelf_homEquiv {X Y : C} (f : X ⟶ Y) : eHomEquiv C f = curry' f :=
  rfl

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

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

Разделы

Аффилиация

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