reflexivePair_hasColimit_of_hasCoequalizer

English

If F.map left and F.map right have a coequalizer, then F has a colimit.

Русский

Если у F.map left и F.map right имеется коэквалайзер, то F имеет колимит.

LaTeX

$$$\text{HasCoequalizer}(F.map\ left, F.map\ right) \Rightarrow \text{HasColimit}(F)$$$

Lean4

instance reflexivePair_hasColimit_of_hasCoequalizer [h : HasCoequalizer (F.map left) (F.map right)] : HasColimit F :=
  hasReflexiveCoequalizer_iff_hasCoequalizer _ |>.mpr h

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