hasLimit_of_hasLimit_comp_eval — Mathlib

English

If F: J ⥤ ∀ i, C_i has limits for every i in I, then F has a limit in the product category.

Русский

Если F: J ⥤ ∏_i C_i имеет пределы в каждой компоненте, то у F есть предел в произведении категорий.

LaTeX

$$$ [\\forall i, HasLimit (F \\cdot (\\Pi.eval C i))] \\Rightarrow HasLimit F $$$

Lean4

/-- If we have a functor `F : J ⥤ Π i, C i` into a category of indexed families,
and we have limits for each of the `F ⋙ Pi.eval C i`,
then `F` has a limit.
-/
theorem hasLimit_of_hasLimit_comp_eval : HasLimit F :=
  HasLimit.mk
    { cone := coneOfConeCompEval fun _ => limit.cone _
      isLimit := coneOfConeEvalIsLimit fun _ => limit.isLimit _ }

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