unop

Mathlib.CategoryTheory.MorphismProperty.Composition

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.IsStableUnderComposition.unop

← MathLib Explorer

English

The unop of a property stable under composition is stable under composition.

Русский

Неопределённое свойство, устойчивое к композиции, остаётся устойчивым под оппонентом.

LaTeX

$$P.unop.IsStableUnderComposition$$

Lean4

instance unop {P : MorphismProperty Cᵒᵖ} [P.IsStableUnderComposition] : P.unop.IsStableUnderComposition where
  comp_mem f g hf hg := P.comp_mem g.op f.op hg hf

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

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

Разделы

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

Аффилиация

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