isIso_ι_of_isColimit' — Mathlib

English

A more general version: for any j and morphism ι: i0 → j, c.ι.app j is an isomorphism when c is a colimit cocone.

Русский

Более общая версия: для любого j и морфизма ι: i0 → j, если c — колимитный конус, то c.ι.app j изоморфизм.

LaTeX

$$IsIso(c.ι.app j)$$

Lean4

/-- More general version of `isIso_ι_of_isColimit`. -/
theorem isIso_ι_of_isColimit' {c : Cocone F} (hc : IsColimit c) (j : J) (ι : i₀ ⟶ j) : IsIso (c.ι.app j) :=
  (h.postcomp ι).isIso_ι_of_isColimit hc

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