isLimitMapConeEmptyConeEquiv — Mathlib

English

IsColimit of G.mapCocone of asEmptyCocone X is equivalent to IsInitial of G.obj X.

Русский

IsColimit (G.mapCocone (asEmptyCocone X)) эквивалентно IsInitial (G.obj X).

LaTeX

$$$\\text{isColimitMapCoconeEmptyCoconeEquiv}(G,X) : \\operatorname{IsColimit}(G.mapCocone(\\mathrm{asEmptyCocone} X)) \\simeq \\operatorname{IsInitial}(G(X)).$$$

Lean4

/-- The map of an empty cone is a limit iff the mapped object is terminal.
-/
def isLimitMapConeEmptyConeEquiv : IsLimit (G.mapCone (asEmptyCone X)) ≃ IsTerminal (G.obj X) :=
  isLimitEmptyConeEquiv D _ _ (eqToIso rfl)

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