of_unop

Mathlib.CategoryTheory.MorphismProperty.Composition

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.IsMultiplicative.of_unop

English

If W on C^op is multiplicative, then W on C is multiplicative.

Русский

Если W на C^{op} мультипликативно, то W на C мультипликативно.

LaTeX

$$$IsMultiplicative(W^{unop}) \Rightarrow IsMultiplicative(W)$$$

Lean4

theorem of_unop (W : MorphismProperty Cᵒᵖ) [IsMultiplicative W.unop] : IsMultiplicative W :=
  (inferInstance : IsMultiplicative W.unop.op)

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

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

Разделы

Аффилиация

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