preservesColimitsOfShape_pempty_of_preservesInitial

English

Preserving the initial object implies preserving all colimits of the empty diagram.

Русский

Сохранение начального объекта влечёт за собой сохранение всех колимитов пустой диаграммы.

LaTeX

$$$[\\text{PreservesColimit}(\\mathrm{empty}, G)] \\Rightarrow \\text{PreservesLimitsOfShape}(\\mathrm{Discrete} \\mathrm{PEmpty}, G).$$$

Lean4

/-- Preserving the initial object implies preserving all colimits of the empty diagram. -/
theorem preservesColimitsOfShape_pempty_of_preservesInitial [PreservesColimit (Functor.empty.{0} C) G] :
    PreservesColimitsOfShape (Discrete PEmpty.{1}) G where
  preservesColimit := preservesColimit_of_iso_diagram G (Functor.emptyExt (Functor.empty.{0} C) _)

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