unit_app_inverse

Mathlib.CategoryTheory.Equivalence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Equivalence.unit_app_inverse

← MathLib Explorer

English

Connects the unit at the inverse object with the counitInv on Y.

Русский

Соединяет единицу на обратном объекте с counitInv на Y.

LaTeX

$$$e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y)$$$

Lean4

theorem unit_app_inverse (e : C ≌ D) (Y : D) : e.unit.app (e.inverse.obj Y) = e.inverse.map (e.counitInv.app Y) := by
  simpa using Iso.comp_hom_eq_id (e.inverse.mapIso (e.counitIso.app Y)) (f := e.unit.app _)

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

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

Разделы

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

Аффилиация

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