hasBinaryCoproducts_of_hasColimit_pair

English

If C has all colimits for diagrams pair X Y, then C has all binary coproducts.

Русский

Если в C существует все копротокольные пределы диаграмм пары X Y, то в C существуют двоичные копродукты.

LaTeX

$$$\forall C\; [HasColimit (pair X Y)]\;\Rightarrow\; HasBinaryCoproducts C$$$

Lean4

/-- If `C` has all colimits of diagrams `pair X Y`, then it has all binary coproducts -/
theorem hasBinaryCoproducts_of_hasColimit_pair [∀ {X Y : C}, HasColimit (pair X Y)] : HasBinaryCoproducts C :=
  { has_colimit := fun F => hasColimit_of_iso (diagramIsoPair F) }

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