natIsoComp

Mathlib.CategoryTheory.Shift.Opposite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.NatTrans.OppositeShift.natIsoComp

Lean4

/-- The obvious isomorphism between `OppositeShift.functor (F ⋙ G)` and the
composition of `OppositeShift.functor F` and `OppositeShift.functor G`.
-/
def natIsoComp : OppositeShift.functor A (F ⋙ G) ≅ OppositeShift.functor A F ⋙ OppositeShift.functor A G :=
  Iso.refl _

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

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

Разделы

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

Аффилиация

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