imageUnopUnop

Mathlib.CategoryTheory.Abelian.Opposite

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

Lean4

/-- The image of `g` is the opposite of the image of `g.unop.` -/
def imageUnopUnop : (image g).unop ≅ image g.unop :=
  (imageUnopOp g).unop

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

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

Разделы

Аффилиация

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