hasColimitsOfShape_of_closedUnderColimitsOfShape

English

HasColimitsOfShape J for P.Comma L R ⊤ ⊤ if J is shape and P.commaObj L R is closed under colimits of shape J.

Русский

Существуют колимиты формы J для P.Comma L R ⊤ ⊤, если J — форма и P.commaObj L R замкнута по колимитам формы J.

LaTeX

$$$$ \\operatorname{HasColimitsOfShape}\\Bigl(J, \\; \\operatorname{Comma}(L,R,\\top,\\top)\\Bigr) $$$$

Lean4

theorem hasColimitsOfShape_of_closedUnderColimitsOfShape [HasColimitsOfShape J (Comma L R)]
    (h : ClosedUnderColimitsOfShape J (P.commaObj L R)) : HasColimitsOfShape J (P.Comma L R ⊤ ⊤) where
  has_colimit _ := hasColimit_of_closedUnderColimitsOfShape _ _ h

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