hasFiniteLimits_of_hasLimitsOfSize₀

Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

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

← MathLib Explorer

English

If HasLimitsOfSize.{0,0} C, then C has finite limits.

Русский

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

LaTeX

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

Lean4

instance (priority := 90) hasFiniteLimits_of_hasLimitsOfSize₀ [HasLimitsOfSize.{0, 0} C] : HasFiniteLimits C :=
  hasFiniteLimits_of_hasLimitsOfSize C

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

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

Разделы

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

Аффилиация

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