hasFiniteCoproducts_of_hasCoproducts

English

If a category has finite coproducts, then it has finite coproducts (trivial rephrasing).

Русский

Если в категории существуют конечные копроизведения, то она имеет конечные копроизведения (переформулировка).

LaTeX

$$$\text{HasFiniteCoproducts } C \Rightarrow \operatorname{HasFiniteCoproducts} C$$$

Lean4

/-- If a category has all coproducts then in particular it has finite coproducts.
-/
theorem hasFiniteCoproducts_of_hasCoproducts [HasCoproducts.{w} C] : HasFiniteCoproducts C :=
  ⟨fun _ => hasColimitsOfShape_of_equivalence (Discrete.equivalence Equiv.ulift.{w})⟩

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