of_op

Mathlib.CategoryTheory.MorphismProperty.Composition

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

English

If W.op.ContainsIdentities, then W.ContainsIdentities.

Русский

Если W.op содержит идентичности, то W содержит идентичности.

LaTeX

$$$W.ContainsIdentities$$$

Lean4

theorem of_op (W : MorphismProperty C) [W.op.ContainsIdentities] : W.ContainsIdentities :=
  (inferInstance : W.op.unop.ContainsIdentities)

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

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

Разделы

Аффилиация

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