hasLimitsOfSize — Mathlib

English

The category of commutative groups has limits of all shapes of the appropriate size; i.e., HasLimitsOfSize holds for CommGrpCat.

Русский

Категория коммутативных групп имеет пределы всех форм подходящего размера; то есть HasLimitsOfSize для CommGrpCat.

LaTeX

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

Lean4

/-- The category of commutative groups has all limits. -/
@[to_additive (relevant_arg := 100) /-- The category of additive commutative groups has all limits. -/
    ]
instance hasLimitsOfSize [UnivLE.{v, u}] : HasLimitsOfSize.{w, v} CommGrpCat.{u} where has_limits_of_shape _ _ := { }

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