hasCoproducts_opposite

Mathlib.CategoryTheory.Limits.Opposites

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.hasCoproducts_opposite

English

If C has products, then C^op has coproducts.

Русский

Если в C существуют произведения, то в C^op существуют копроизведения.

LaTeX

$$$[HasProducts C] \\Rightarrow [HasCoproducts (C^{\\mathrm{op}})]$$$

Lean4

instance hasCoproducts_opposite [HasProducts.{v₂} C] : HasCoproducts.{v₂} Cᵒᵖ := fun _ => inferInstance

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

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

Разделы

Аффилиация

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