uniq_cocone_morphism — Mathlib

English

If t is a colimit cocone, then any two cocone morphisms f, f' from t to the same cocone s are equal; the colimit cocone has a unique morphism out to any other cocone.

Русский

Если t — колимитный кокон, то любые два кокон-морфизма f, f' из t в один и тот же кокон s совпадают; колимитный кокон имеет единственный исходный морфизм к любому кокону.

LaTeX

$$$ \forall {s,t : Cocone F} (h : IsColimit t) {f f' : t ⟶ s}, f = f' $$$

Lean4

theorem uniq_cocone_morphism {s t : Cocone F} (h : IsColimit t) {f f' : t ⟶ s} : f = f' :=
  have : ∀ {g : t ⟶ s}, g = h.descCoconeMorphism s := by intro g; ext; exact h.uniq _ _ g.w
  this.trans this.symm

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