hasFiniteCoproducts_of_hasFiniteColimits

English

If a category has all coproducts, then it has finite coproducts.

Русский

Если категория имеет все копроизведения, то она имеет конечные копроизведения.

LaTeX

$$$[\text{HasCoproducts } C] \Rightarrow \operatorname{HasFiniteCoproducts} C$$$

Lean4

/-- If `C` has finite colimits then it has finite coproducts. -/
instance (priority := 10) hasFiniteCoproducts_of_hasFiniteColimits [HasFiniteColimits C] : HasFiniteCoproducts C :=
  ⟨fun J => by infer_instance⟩

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