hasEqualizers_of_hasWideEqualizers

English

Two maps into the wide equalizer are equal if they agree after composing with the wide equalizer projection.

Русский

Два отображения в широкий эквалайзер равны, если они совпадают после композиции с проекцией широкого эквалайзера.

LaTeX

$$$\forall k,l : wideEqualizer f ⟶ W,\ (wideEqualizer.π f) \circ k = (wideEqualizer.π f) \circ l \Rightarrow k = l$$$

Lean4

instance (priority := 10) hasEqualizers_of_hasWideEqualizers [HasWideEqualizers.{w} C] : HasEqualizers C :=
  hasLimitsOfShape_of_equivalence.{w} walkingParallelFamilyEquivWalkingParallelPair

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