hasColimitsOfSize — Mathlib

English

If J has colimits in A and G preserves them, then CostructuredArrow G X has colimits of shape J.

Русский

Если J имеет колимиты в A и G сохраняет их, то CostructuredArrow G X имеет колимиты формы J.

LaTeX

$$$\\operatorname{HasColimitsOfShape}(J,\\mathrm{CostructuredArrow}\\, G\\, X)$$$

Lean4

instance hasColimitsOfSize [HasColimitsOfSize.{w, w'} A] [PreservesColimitsOfSize.{w, w'} G] :
    HasColimitsOfSize.{w, w'} (CostructuredArrow G X) :=
  ⟨fun _ _ => inferInstance⟩

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