colimitsOfShape_le_coproducts — Mathlib

English

For any W, the colimits of shapeDiscrete J are contained in coproducts of W; i.e., colimits over a discrete diagram can be realized as a coproduct.

Русский

Для любого W колимиты формы Discrete J вложены в копроодукты W; то есть колимит диаграммы, дискретной по форме, реализуется как копродукт.

LaTeX

$$$W.colimitsOfShape(Discrete J) \le coproducts(W)$$$

Lean4

theorem colimitsOfShape_le_coproducts (J : Type w) : W.colimitsOfShape (Discrete J) ≤ coproducts.{w} W :=
  le_iSup (f := fun (J : Type w) ↦ W.colimitsOfShape (Discrete J)) J

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