instHasColimitsOfShapeUnderOfWithInitial

Mathlib.CategoryTheory.WithTerminal.Cone

URI: https://scilib.ai/kg/mathlib#instHasColimitsOfShapeUnderOfWithInitial

← MathLib Explorer

English

If C has colimits of shape WithInitial J, then Under X has colimits of shape J.

Русский

Если в C существуют колимиты заданной формы WithInitial J, то в Under X существуют колимиты формы J.

LaTeX

$$HasColimitsOfShape J (Under X)$$

Lean4

instance (X : C) [HasColimitsOfShape (WithInitial J) C] : HasColimitsOfShape J (Under X) where
  has_colimit _ := Under.hasColimit_of_hasColimit_liftFromUnder ..

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

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

Разделы

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

Аффилиация

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