le_coproducts

Mathlib.CategoryTheory.MorphismProperty.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.le_coproducts

English

Every W is included in the coproducts of W, i.e., W ≤ coproducts W.

Русский

Любое W включено в копродукты W, то есть W ≤ coproducts W.

LaTeX

$$W \le coproducts(W)$$

Lean4

theorem le_coproducts : W ≤ coproducts.{w} W :=
  (le_colimitsOfShape_punit.{w} W).trans (colimitsOfShape_le_coproducts W PUnit.{w + 1})

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru