hasProducts_of_opposite

Mathlib.CategoryTheory.Limits.Opposites

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

English

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

Русский

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

LaTeX

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

Lean4

theorem hasProducts_of_opposite [HasCoproducts.{v₂} Cᵒᵖ] : HasProducts.{v₂} C := fun X =>
  hasProductsOfShape_of_opposite X

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

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

Разделы

Аффилиация

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