liftConeMorphism_eq_isTerminal_from

English

For a limit cone c and any cone s, the liftConeMorphism from hc (IsLimit c) to s equals IsTerminal.from of the corresponding isTerminal equivalence.

Русский

Для пределного конуса c и любого конуса s, liftConeMorphism от hc к s равен IsTerminal.from соответствующему эквивалентному преобразованию.

LaTeX

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

Lean4

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

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