hasCoproductsOfShape_of_hasBiproductsOfShape

English

If J-biproducts exist in C, then C has coproducts of shape J.

Русский

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

LaTeX

$$$\forall J\ C,[HasBiproductsOfShape(J, C)]\Rightarrow HasCoproductsOfShape(J, C)$$$

Lean4

instance (priority := 100) hasCoproductsOfShape_of_hasBiproductsOfShape [HasBiproductsOfShape J C] :
    HasCoproductsOfShape J C where has_colimit _ := hasColimit_of_iso Discrete.natIsoFunctor

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