of_hasBinaryCoproduct' — Mathlib

English

If X and Y have a binary coproduct and an initial object exists, then the pushout from the initial object to X and Y via coprod.inl and coprod.inr is a pushout.

Русский

Если существуют двоичный coproduct X ⊔ Y и начальный объект, то предел по началу к X,Y через coprod.inl, coprod.inr является пределом.

LaTeX

$$$ [HasBinaryCoproduct X Y] [HasInitial C] : IsPushout (initial.to X) (initial.to Y) (coprod.inl) (coprod.inr) $$$

Lean4

theorem of_hasBinaryCoproduct' [HasBinaryCoproduct X Y] [HasInitial C] :
    IsPushout (initial.to _) (initial.to _) (coprod.inl : X ⟶ _) (coprod.inr : Y ⟶ _) :=
  of_is_coproduct (colimit.isColimit _) initialIsInitial

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