hasLimitsOfShape — Mathlib

English

If J is a small category, then CommSemiRingCat has limits of shape J; i.e., for every functor F : J ⥤ CommSemiRingCat there is a limit of shape J.

Русский

Пусть J — маленькая категория; тогда в CommSemiRingCat существуют пределы формы J.

LaTeX

$$$ \\text{HasLimitsOfShape } J\\ CommSemiRingCat$$$

Lean4

/-- If `J` is `u`-small, `CommSemiRingCat.{u}` has limits of shape `J`. -/
instance hasLimitsOfShape [Small.{u} J] : HasLimitsOfShape J CommSemiRingCat.{u} where

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