instPreservesColimitπ₃ — Mathlib

English

For F : J ⥤ ShortComplex C with π₁, π₂, π₃ having colimits, F preserves the colimit π₃.

Русский

Для F: J ⥤ ShortComplex C, если существуют колимиты для π₁, π₂, π₃, F сохраняет колимит π₃.

LaTeX

$$$ \text{PreservesColimit } F \pi_3 $$$

Lean4

noncomputable instance : PreservesColimit F π₃ :=
  preservesColimit_of_preserves_colimit_cocone (isColimitColimitCocone F) (isColimitπ₃MapCoconeColimitCocone F)

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