IsIsomorphic

Mathlib.CategoryTheory.IsomorphismClasses

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

Lean4

/-- An object `X` is isomorphic to an object `Y`, if `X ≅ Y` is not empty. -/
def IsIsomorphic : C → C → Prop := fun X Y => Nonempty (X ≅ Y)

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

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

Разделы

Аффилиация

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