preservesLimitsOfShape_of_initial

English

If HasLimitsOfShape C E and F is initial, then HasLimitsOfShape D E.

Русский

Если есть пределы в форме C в E и F начальная, тогда есть пределы в форме D в E.

LaTeX

$$$[HasLimitsOfShape C E] \\Rightarrow [HasLimitsOfShape D E]$, via the map F.$$

Lean4

theorem preservesLimitsOfShape_of_initial {B : Type u₄} [Category.{v₄} B] (H : E ⥤ B) [PreservesLimitsOfShape C H] :
    PreservesLimitsOfShape D H where preservesLimit := preservesLimit_of_comp F

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