isColimitExtendCoconeEquiv — Mathlib

English

Iso F F' implies Initial F iff Initial F'.

Русский

Изоморфизм F ≅ F' влечёт эквиваленцию: Initial F ⇔ Initial F'.

LaTeX

$$$$ \operatorname{Initial}(F) \iff \operatorname{Initial}(F'). $$$$

Lean4

/-- When `F` is final, and `t : Cocone (F ⋙ G)`,
`extendCocone.obj t` is a colimit cocone exactly when `t` is.
-/
def isColimitExtendCoconeEquiv (t : Cocone (F ⋙ G)) : IsColimit (extendCocone.obj t) ≃ IsColimit t :=
  IsColimit.ofCoconeEquiv (coconesEquiv F G)

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