hasLimits_of_hasColimits_op — Mathlib

English

If HasColimitsOfShape (Opposite J) (C), then HasLimitsOfShape J C.

Русский

Если у категории C есть колимиты формы Opposite J, то у C существуют пределы формы J.

LaTeX

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

Lean4

theorem hasLimits_of_hasColimits_op [HasColimitsOfSize.{v₂, u₂} Cᵒᵖ] : HasLimitsOfSize.{v₂, u₂} C :=
  { has_limits_of_shape := fun _ _ => hasLimitsOfShape_of_hasColimitsOfShape_op }

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