hasLimitsOfSize — Mathlib

English

The category of monoids has all limits (i.e., HasLimits MonCat).

Русский

Категория моноидов имеет все пределы (HasLimits MonCat).

LaTeX

$$$\text{HasLimits }\text{MonCat}$$$

Lean4

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

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