hasFiniteCoproducts_opposite — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance hasFiniteCoproducts_opposite [HasFiniteProducts C] : HasFiniteCoproducts Cᵒᵖ where
  out _ := Limits.hasCoproductsOfShape_opposite _

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