from_eq_liftConeMorphism — Mathlib

English

Dual to the previous, the terminal cone hc corresponds to liftConeMorphism via the symmetrized isLimit equivalence.

Русский

Двойственный случай: терминальный конус hc соответствует liftConeMorphism через симметрическое эквивалентное преобразование isLimit.

LaTeX

$$$\\mathrm{IsTerminal.from}\\;\\hc\\;s = ((\\mathrm{Cone.isLimitEquivIsTerminal}\\, _).symm\\;hc).liftConeMorphism\\;s$$$

Lean4

theorem from_eq_liftConeMorphism {F : J ⥤ C} {c : Cone F} (hc : IsTerminal c) (s : Cone F) :
    IsTerminal.from hc s = ((Cone.isLimitEquivIsTerminal _).symm hc).liftConeMorphism s :=
  (IsLimit.liftConeMorphism_eq_isTerminal_from (c.isLimitEquivIsTerminal.symm hc) s).symm

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