hasSmallestLimitsOfHasLimits

Mathlib.CategoryTheory.Limits.HasLimits

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

English

If a category C has all limits, then it has all limits of size (0,0).

Русский

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

LaTeX

$$$\\text{HasLimitsOfSize}(C)$$$

Lean4

instance (priority := 100) hasSmallestLimitsOfHasLimits [HasLimits C] : HasLimitsOfSize.{0, 0} C :=
  hasLimitsOfSizeShrink.{0, 0} C

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

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

Разделы

Аффилиация

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