isLimitLimitCone

Mathlib.Algebra.Homology.ShortComplex.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.isLimitLimitCone

Lean4

/-- `limitCone F` is limit. -/
noncomputable def isLimitLimitCone : IsLimit (limitCone F) :=
  isLimitOfIsLimitπ _ (isLimitπ₁MapConeLimitCone F) (isLimitπ₂MapConeLimitCone F) (isLimitπ₃MapConeLimitCone F)

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

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

Разделы

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

Аффилиация

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