hasColimitsOfShape_of_hasLimitsOfShape_op

English

If HasLimitsOfShape (J^op) C^op holds, then HasColimitsOfShape J C.

Русский

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

LaTeX

$$$\\text{HasColimitsOfShape }J\\, C \\;\\text{given }\\; [\\text{HasLimitsOfShape }J^{\\mathrm{op}} C^{\\mathrm{op}}]$$$

Lean4

theorem hasColimitsOfShape_of_hasLimitsOfShape_op [HasLimitsOfShape Jᵒᵖ Cᵒᵖ] : HasColimitsOfShape J C :=
  { has_colimit := fun F => hasColimit_of_hasLimit_op F }

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