hasLimitOfHasLimitsOfShape — Mathlib

English

If C has limits and J is a small shape with HasLimitsOfShape J C, then for any functor F : J ⥤ C, F has a limit. This provides an instance HasLimit F.

Русский

Если у C есть пределы, и HasLimitsOfShape J C, то F : J ⥤ C имеет предел; образуется экземпляр HasLimit F.

LaTeX

$$$\\text{HasLimit F}$$$

Lean4

instance (priority := 100) hasLimitOfHasLimitsOfShape {J : Type u₁} [Category.{v₁} J] [HasLimitsOfShape J C]
    (F : J ⥤ C) : HasLimit F :=
  HasLimitsOfShape.has_limit F

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