hom_ext — Mathlib

English

If s is a limit cone, then two morphisms into s.pt are equal whenever their compositions with s.fst and s.snd agree.

Русский

Если s является пределом, то две морфизмa из W в s.pt равны, когда их композиции с s.fst и s.snd совпадают.

LaTeX

$$$$ \forall f,g: W \to s.pt,\ f\circ s.fst = g\circ s.fst \land f\circ s.snd = g\circ s.snd \Rightarrow f=g. $$$$

Lean4

theorem hom_ext {W X Y : C} {s : BinaryFan X Y} (h : IsLimit s) {f g : W ⟶ s.pt} (h₁ : f ≫ s.fst = g ≫ s.fst)
    (h₂ : f ≫ s.snd = g ≫ s.snd) : f = g :=
  h.hom_ext fun j => Discrete.recOn j fun j => WalkingPair.casesOn j h₁ h₂

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