instHasLimitsOfShape — Mathlib

English

If J is a shape, and J has limits in C, then the category of simplicial objects in C has limits of shape J.

Русский

Если для формы J в C существуют пределы, то в категории simplicial objects(C) тоже существуют пределы формы J.

LaTeX

$$$HasLimitsOfShape J (SimplicialObject C)\\;\\text{given}\\; HasLimitsOfShape J C$$$

Lean4

instance {J : Type v} [SmallCategory J] [HasLimitsOfShape J C] : HasLimitsOfShape J (SimplicialObject C) :=
  by
  dsimp [SimplicialObject]
  infer_instance

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