hom_ext — Mathlib

English

If two arrows into the wide equalizer are equal after composing with the wide equalizer projection π f, then they are equal.

Русский

Если две стрелки в широкий эквалайзер совпадают после композиции с π f, то они равны.

LaTeX

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

Lean4

/-- Two maps into a wide equalizer are equal if they are equal when composed with the wide
    equalizer map. -/
@[ext]
theorem hom_ext [Nonempty J] {W : C} {k l : W ⟶ wideEqualizer f} (h : k ≫ wideEqualizer.ι f = l ≫ wideEqualizer.ι f) :
    k = l :=
  Trident.IsLimit.hom_ext (limit.isLimit _) h

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