hom_ext — Mathlib

English

If s is an IsLimit for a Trident f and two arrows k, l into s.pt satisfy k ≫ ι = l ≫ ι, then k = l.

Русский

Если s является пределом (IsLimit) для тридента f и две стрелки k, l в s.pt удовлетворяют k ≫ ι = l ≫ ι, тогда k = l.

LaTeX

$$$\forall k, l: W \to s.pt,\ k ≫ s.ι = l ≫ s.ι \Rightarrow k = l$$$

Lean4

theorem hom_ext [Nonempty J] {s : Trident f} (hs : IsLimit s) {W : C} {k l : W ⟶ s.pt} (h : k ≫ s.ι = l ≫ s.ι) :
    k = l :=
  hs.hom_ext <| Trident.equalizer_ext _ h

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