expUnitIsoSelf

Mathlib.CategoryTheory.Closed.Cartesian

URI: https://scilib.ai/kg/mathlib#CategoryTheory.expUnitIsoSelf

Lean4

/-- The exponential of any object with the terminal object is isomorphic to itself, i.e. `X^1 ≅ X`.
The typeclass argument is explicit: any instance can be used. -/
def expUnitIsoSelf [Exponentiable (𝟙_ C)] : (𝟙_ C) ⟹ X ≅ X :=
  (expUnitNatIso.app X).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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