hasCoproductsOfShape_of_hasCoproducts

English

If C has all small coproducts, then for every index shape J, C has coproducts of shape J.

Русский

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

LaTeX

$$$\forall J,\ HasCoproductsOfShape J\ C$$$

Lean4

instance (priority := 100) hasCoproductsOfShape_of_hasCoproducts [HasCoproducts.{w} C] (J : Type w) :
    HasCoproductsOfShape J C :=
  inferInstance

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