hasLimitsOfShape — Mathlib

English

If C has limits of shape J, then the category of monoids in C, Mon C, also has limits of shape J.

Русский

Если у категории C есть пределы формы J, то Mon C также имеет пределы формы J.

LaTeX

$$$ \text{HasLimitsOfShape } J (Mon C)$$$

Lean4

instance hasLimitsOfShape [HasLimitsOfShape J C] : HasLimitsOfShape J (Mon C) where
  has_limit := fun F =>
    HasLimit.mk
      { cone := limitCone F
        isLimit := limitConeIsLimit F }

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