instHasLimitsOfShapeDiscreteInd — Mathlib

English

For any small C and any discrete shape J, the Ind-category has limits of shape Discrete(J).

Русский

Для любой небольшой категории C и любой форме Discrete(J) Ind-пусть имеет пределы формы Discrete(J).

LaTeX

$$$\text{HasLimitsOfShape}(\mathrm{Discrete}(J), \mathrm{Ind}(C))$$$

Lean4

instance {J : Type v} [HasLimitsOfShape (Discrete J) C] : HasLimitsOfShape (Discrete J) (Ind C) :=
  hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (Ind.inclusion C)

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