hasFiniteProducts_opposite

Mathlib.CategoryTheory.Limits.Opposites

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

English

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

Русский

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

LaTeX

$$$[HasFiniteProducts C] \\Rightarrow [HasFiniteCoproducts (C^{\\mathrm{op}})]$$$

Lean4

instance hasFiniteProducts_opposite [HasFiniteCoproducts C] : HasFiniteProducts Cᵒᵖ where out _ := inferInstance

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

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

Разделы

Аффилиация

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