uniq_cone_morphism — Mathlib

English

Let t be a limit cone for F and s be any cone over F. Then there exists at most one morphism f: s ⟶ t; i.e., any two cone morphisms from s to t are equal.

Русский

Пусть t — предел конуса над F, а s — любой конус над F. Тогда существует не более одного морфизма f: s ⟶ t, то есть любые два конусных морфизма из s в t совпадают.

LaTeX

$$$\\forall s,t\\,(h:\\mathrm{IsLimit}\\,t)\\;\\forall f,f':s\\to t,\; f=f'.$$$

Lean4

theorem uniq_cone_morphism {s t : Cone F} (h : IsLimit t) {f f' : s ⟶ t} : f = f' :=
  have : ∀ {g : s ⟶ t}, g = h.liftConeMorphism s := by intro g; apply ConeMorphism.ext; exact h.uniq _ _ g.w
  this.trans this.symm

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