instHasCofilteredLimitsOfSizeFunctor

English

If C has cofiltered limits of size (w', w), then the functor category K ⥤ C has cofiltered limits of the same size.

Русский

Если у C существуют когейло-ограниченные пределы заданного размера (w', w), то K ⥤ C имеет соответствующие кофильтрованные пределы.

LaTeX

$$$\\text{HasCofilteredLimitsOfSize}_{w',w}(K \\;⥤\\; C).$$$

Lean4

instance [HasCofilteredLimitsOfSize.{w', w} C] : HasCofilteredLimitsOfSize.{w', w} (K ⥤ C) :=
  ⟨fun _ => inferInstance⟩

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