functorCategoryHasLimitsOfSize — Mathlib

English

There is an instance HasLimitsOfSize for functor categories when the underlying category C has limits of the corresponding sizes

Русский

Существует HasLimitsOfSize для категорий функторов, если в C существуют пределы соответствующих размеров

LaTeX

$$$\\text{HasLimitsOfSize }{\\lbrace v, u \\rbrace} (\\mathrm{Functor } K C)$$$

Lean4

instance functorCategoryHasLimitsOfSize [HasLimitsOfSize.{v₁, u₁} C] : HasLimitsOfSize.{v₁, u₁} (K ⥤ C) where
  has_limits_of_shape := inferInstance

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