imageOpUnop

Mathlib.CategoryTheory.Abelian.Opposite

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

Lean4

/-- The image of `f.op` is the opposite of the image of `f`. -/
def imageOpUnop : (image f.op).unop ≅ image f :=
  (imageUnopOp f.op).unop

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

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

Разделы

Аффилиация

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