hasBinaryCoproduct_zero_left — Mathlib

English

There exists a binary coproduct of the zero object with any object X in a category with zero objects and zero morphisms.

Русский

Существет бинарное копроизведение нулевого объекта и любого объекта X в категории с нулевыми объектами и нулевыми морфизмами.

LaTeX

$$$$ \text{HasBinaryCoproduct}(0,X) $$$$

Lean4

instance hasBinaryCoproduct_zero_left (X : C) : HasBinaryCoproduct (0 : C) X :=
  HasColimit.mk ⟨_, binaryCofanZeroLeftIsColimit X⟩

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