hasProductsOfShape_of_hasBiproductsOfShape

English

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

Русский

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

LaTeX

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

Lean4

instance (priority := 100) hasProductsOfShape_of_hasBiproductsOfShape [HasBiproductsOfShape J C] :
    HasProductsOfShape J C where has_limit _ := hasLimit_of_iso Discrete.natIsoFunctor.symm

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