instTransIso

Mathlib.CategoryTheory.Iso

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Iso.instTransIso

Lean4

@[simps]
instance instTransIso : Trans (α := C) (· ≅ ·) (· ≅ ·) (· ≅ ·) where trans := trans

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

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

Разделы

Аффилиация

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