hasLimitsOfShape — Mathlib

English

HasLimitsOfShape J (Action V G) whenever J is a category and V has limits of shape J.

Русский

Пределы формы J в Action V G существуют, если J — категория и V имеет пределы формы J.

LaTeX

$$$\operatorname{HasLimitsOfShape}(J, \mathrm{Action}(V,G)).$$$

Lean4

/-- If `V` has limits of shape `J`, so does `Action V G`. -/
instance hasLimitsOfShape {J : Type*} [Category J] [HasLimitsOfShape J V] : HasLimitsOfShape J (Action V G) :=
  Adjunction.hasLimitsOfShape_of_equivalence (Action.functorCategoryEquivalence _ _).functor

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