mk

Mathlib.CategoryTheory.Limits.Shapes.Biproducts

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

English

From a limit-bicone, one obtains a biproduct structure for the index family.

Русский

Из лимитного биконеуса получаем структуру бипродукта для данной семейства индексов.

LaTeX

$$$$ \\text{HasBiproduct}(F) \\quad\\text{from}\\quad d: \\text{LimitBicone}(F). $$$$

Lean4

theorem mk {F : J → C} (d : LimitBicone F) : HasBiproduct F :=
  ⟨Nonempty.intro d⟩

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

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

Разделы

Аффилиация

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