hasFiniteColimits_of_hasColimitsOfSize₀

Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.hasFiniteColimits_of_hasColimitsOfSize₀

← MathLib Explorer

English

If HasLimitsOfSize.{0,0} C, then HasFiniteLimits C.

Русский

Если существуют пределы размеров 0,0, то существуют конечные пределы.

LaTeX

$$$\operatorname{HasLimitsOfSize}_{0,0}(C) \Rightarrow \operatorname{HasFiniteLimits}(C)$$$

Lean4

instance (priority := 90) hasFiniteColimits_of_hasColimitsOfSize₀ [HasColimitsOfSize.{0, 0} C] : HasFiniteColimits C :=
  hasFiniteColimits_of_hasColimitsOfSize C

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

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

Разделы

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

Аффилиация

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