hasLimitsOfShape — Mathlib

English

The category of commutative groups has all limits of size bounded by universes; i.e., it has limits of shape J for all J in the appropriate universe.

Русский

Категория коммукатегории групп имеет пределы всех размерами, ограниченные по вселенным; то есть пределы по форме J существуют для всех J в допустимом вселенной.

LaTeX

$$$ \mathrm{HasLimitsOfSize}(J, \mathrm{CommGrpCat}) $ for all small J$$

Lean4

/-- If `J` is `u`-small, `CommGrpCat.{u}` has limits of shape `J`. -/
@[to_additive /-- If `J` is `u`-small, `AddCommGrpCat.{u}` has limits of shape `J`. -/
    ]
instance hasLimitsOfShape [Small.{u} J] : HasLimitsOfShape J CommGrpCat.{u} where has_limit _ := inferInstance

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