hasLimitsOfSize — Mathlib

English

The category GrpCat has all limits (i.e., limits of every shape).

Русский

Категория GrpCat имеет все пределы (пределы для любых форм).

LaTeX

$$$ \forall J\, [\text{Small}(J) \Rightarrow \mathrm{HasLimitsOfShape}(J, \mathrm{GrpCat})]$$$

Lean4

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

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