hasPushout_biprod_fst_biprod_snd — Mathlib

English

A duplicated statement of a pushout for the biproduct skeleton; the square with biprod.inl and biprod.inr is pushout.

Русский

Дублирующее утверждение пушаута для би-произведения; квадрат biprod.inl и biprod.inr является пушаутом.

LaTeX

$$$\operatorname{IsPushout}(\mathrm{biprod}.\mathrm{fst}, \mathrm{biprod}.\mathrm{snd}, 0, 0)$$$

Lean4

instance hasPushout_biprod_fst_biprod_snd [HasBinaryBiproduct X Y] :
    HasPushout (biprod.fst : _ ⟶ X) (biprod.snd : _ ⟶ Y) :=
  HasColimit.mk ⟨_, (of_hasBinaryBiproduct X Y).isColimit⟩

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