op

Mathlib.CategoryTheory.MorphismProperty.Composition

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.ContainsIdentities.op

English

If W contains identities, so does W.op (the opposite property).

Русский

Если свойство содержит идентичности, то и его противоположное свойство содержит идентичности.

LaTeX

$$$W^{op}.ContainsIdentities$$$

Lean4

instance op (W : MorphismProperty C) [W.ContainsIdentities] : W.op.ContainsIdentities :=
  ⟨fun X => W.id_mem X.unop⟩

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

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

Разделы

Аффилиация

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