instHasCoproducts — Mathlib

English

If C has terminal objects, then the FormalCoproduct construction gives HasCoproducts for FormalCoproduct C; i.e., the category FormalCoproduct C has all coproducts indexed by any type.

Русский

Если в C есть терминальные объекты, то построение FormalCoproduct обеспечивает наличие копроизводных для FormalCoproduct C; то есть категория FormalCoproduct C имеет все копроизводные, индексируемые по любому типу.

LaTeX

$$$\\mathrm{HasCoproducts}(\\mathrm{FormalCoproduct}\\; C)$$$

Lean4

instance : HasCoproducts.{w} (FormalCoproduct.{w} C) :=
  hasCoproducts_of_colimit_cofans _ (isColimitCofan _)

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