instHasLimit — Mathlib

English

The category ProfiniteGrp has limits: for every small category J and functor F: J ⥤ ProfiniteGrp, a limit cone exists with a specified cone and universal property.

Русский

Категория ProfiniteGrp имеет пределы: для любой малой категории J и функторa F: J ⥤ ProfiniteGrp существует предел и соответствующее единство.

LaTeX

$$$\forall J [\text{SmallCategory } J] (F: J \to \mathrm{ProfiniteGrp}), \; \exists \text{limit cone of } F$$$

Lean4

instance : Limits.HasLimit F where
  exists_limit :=
    Nonempty.intro
      { cone := limitCone F
        isLimit := limitConeIsLimit F }

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