hasEqualizer_of_hasSplitEqualizer

English

If a pair has a split equalizer, then it has an equalizer; the splitting provides the universal equalizer cone.

Русский

Если пара имеет разложённый эквалайзер, то он имеет эквалайзер; разложение обеспечивает всепринимающее коно-эквалайзер.

LaTeX

$$$[HasSplitEqualizer f g] \\Rightarrow HasEqualizer f g$$$

Lean4

/-- If a pair has a split equalizer, it has a equalizer. -/
instance (priority := 1) hasEqualizer_of_hasSplitEqualizer [HasSplitEqualizer f g] : HasEqualizer f g :=
  HasLimit.mk ⟨_, (HasSplitEqualizer.isSplitEqualizer f g).isEqualizer⟩

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