hasLimitsOfSize — Mathlib

English

The category CommMonCat has all limits when the universe allows it (HasLimitsOfSize).

Русский

Категория CommMonCat имеет все пределы, когда это допускается вселенной (HasLimitsOfSize).

LaTeX

$$$\text{HasLimitsOfSize }\text{CommMonCat}$$$

Lean4

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

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