hasLimitsOfShape — Mathlib

English

For any category J and any functor F: J ⥤ MonCat, MonCat has a limit of shape J provided J is small in the universe.

Русский

Для любой категории J и любой функтор F: J ⥤ MonCat, MonCat имеет предел формы J, если J является маленькой по вселенной.

LaTeX

$$$\text{HasLimitsOfShape } J\ MonCat$$$

Lean4

/-- If `J` is `u`-small, `MonCat.{u}` has limits of shape `J`. -/
@[to_additive /-- If `J` is `u`-small, `AddMonCat.{u}` has limits of shape `J`. -/
    ]
instance hasLimitsOfShape [Small.{u} J] : HasLimitsOfShape J MonCat.{u} where has_limit _ := inferInstance

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