hasCoproductsOfShape_of_opposite — Mathlib

English

If Opposite C has products of shape X, then C has coproducts of shape X.

Русский

Если в Opposite C существуют произведения формы X, то в C существуют копроизведения формы X.

LaTeX

$$$[HasProductsOfShape X (C^{\\mathrm{op}})] \\Rightarrow [HasCoproductsOfShape X C]$$$

Lean4

theorem hasCoproductsOfShape_of_opposite [HasProductsOfShape X Cᵒᵖ] : HasCoproductsOfShape X C :=
  haveI : HasLimitsOfShape (Discrete X)ᵒᵖ Cᵒᵖ := hasLimitsOfShape_of_equivalence (Discrete.opposite X).symm
  hasColimitsOfShape_of_hasLimitsOfShape_op

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