instHasLimitProd — Mathlib

English

The limit of a functor G: J × K ⥤ C exists provided C has limits of shape K and the curry-application combined with lim has a limit. In particular, HasLimit G holds under these hypotheses.

Русский

Предел диаграммы G: J×K ⥤ C существует, если в C существуют пределы формы K и если предел curry(obj G) ⋙ lim существует; тогда существует предел G.

LaTeX

$$$[HasLimitsOfShape K C] \\wedge [HasLimit (\\text{curry.obj } G \\;\\gg\\; \\lim)] \\Rightarrow HasLimit G$$$

Lean4

/-- The functor `G` has a limit if `C` has `K`-shaped limits and `(curry.obj G ⋙ lim)` has a limit.
-/
instance : HasLimit G where
  exists_limit :=
    ⟨{  cone := coneOfHasLimitCurryCompLim G
        isLimit := isLimitConeOfHasLimitCurryCompLim G }⟩

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