unop_isoClosure

Mathlib.CategoryTheory.ObjectProperty.Opposite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.unop_isoClosure

← MathLib Explorer

English

Opposite of isoClosure equals isoClosure of unop: P.isoClosure.unop = P.unop.isoClosure.

Русский

Обратное к isoClosure равно isoClosure от unop: P.isoClosure.unop = P.unop.isoClosure.

LaTeX

$$$P.isoClosure.unop = P.unop.isoClosure$$$

Lean4

theorem unop_isoClosure (P : ObjectProperty Cᵒᵖ) : P.isoClosure.unop = P.unop.isoClosure := by
  rw [← op_injective_iff, P.unop.op_isoClosure, op_unop, op_unop]

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

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

Разделы

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

Аффилиация

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