hasLimitsOfShape_of_hasColimitsOfShape_op

English

If C^op has colimits of shape J^op, then C has limits of shape J.

Русский

Если в C^op существуют колимиты формы J^op, то в C существуют пределы формы J.

LaTeX

$$$$\\mathrm{HasLimitsOfShape}(J, C) \\text{ follows from } \\mathrm{HasColimitsOfShape}(J^{op}, C^{op}).$$$$

Lean4

theorem hasLimitsOfShape_of_hasColimitsOfShape_op [HasColimitsOfShape Jᵒᵖ Cᵒᵖ] : HasLimitsOfShape J C :=
  { has_limit := fun F => hasLimit_of_hasColimit_op F }

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