total

Mathlib.CategoryTheory.Preadditive.Biproducts

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

← MathLib Explorer

English

If a finite bicone satisfies the total condition, it becomes a bilimit.

Русский

Если конечный биоконит удовлетворяет условию total, он становится билимитом.

LaTeX

$$isBilimitOfTotal b total$$

Lean4

theorem total {f : J → C} {b : Bicone f} (i : b.IsBilimit) : ∑ j : J, b.π j ≫ b.ι j = 𝟙 b.pt :=
  i.isLimit.hom_ext fun j => by
    classical
    cases j
    simp [sum_comp, b.ι_π, comp_dite]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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