hasCoproducts

Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SmallObject.hasCoproducts

English

Under the same hypotheses, coproducts exist in the category C.

Русский

Существуют копродукты в категории C.

LaTeX

$$$\\mathrm{HasCoproducts}(C)$$$

Lean4

theorem hasCoproducts : HasCoproducts.{w} C :=
  IsCardinalForSmallObjectArgument.hasCoproducts I κ

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

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

Разделы

Аффилиация

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