hasTerminalChangeUniverse — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem hasTerminalChangeUniverse [h : HasLimitsOfShape (Discrete.{w} PEmpty) C] :
    HasLimitsOfShape (Discrete.{w'} PEmpty) C where has_limit _ := hasTerminalChangeDiagram C (h.1 (Functor.empty C))

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