hasInitialChangeUniverse — Mathlib

English

If a category C has colimits of shape Discrete PEmpty in one universe, then it has those colimits in another universe as well.

Русский

Если у категории C существуют колимиты формы Discrete PEmpty в одной вселенной, то они существуют и в другой вселенной.

LaTeX

$$$[\\mathrm{HasColimitsOfShape}(\\mathrm{Discrete}(PEmpty))\, C] \\Rightarrow [\\mathrm{HasColimitsOfShape}(\\mathrm{Discrete}(PEmpty))\, C].$$$

Lean4

theorem hasInitialChangeUniverse [h : HasColimitsOfShape (Discrete.{w} PEmpty) C] :
    HasColimitsOfShape (Discrete.{w'} PEmpty) C where has_colimit _ := hasInitialChangeDiagram C (h.1 (Functor.empty C))

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