hasLimitsOfShape_of_has_cofiltered_limits

English

If C has cofiltered limits of a certain size, then for any I that is cofiltered, C has limits of shape I.

Русский

Если в C существуют кофильтрованные пределы заданного размера, то для любого индекса I, являющегося кофильтрованным, C имеет пределы формы I.

LaTeX

$$$[HasCofilteredLimitsOfSize^{w',w} C] \Rightarrow [HasLimitsOfShape I C]$ for any I with IsCofiltered I$$

Lean4

instance (priority := 100) hasLimitsOfShape_of_has_cofiltered_limits [HasCofilteredLimitsOfSize.{w', w} C] (I : Type w)
    [Category.{w'} I] [IsCofiltered I] : HasLimitsOfShape I C :=
  HasCofilteredLimitsOfSize.HasLimitsOfShape _

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