hasColimitsOfShape_of_isSuccLimit

English

Let j be an index in a linear order J, and suppose there is a successor-limit structure on a chosen target α; then there are colimits of shape α in C.

Русский

Пусть j — индекс в линейном порядке J, и пусть на выбранной цели α задана структура перехода к succ-ограниченному пределу; тогда существуют колимиты формы α в C.

LaTeX

$$$\mathrm{HasColimitsOfShape}(\alpha, C)$, при условии существования j и hj$$

Lean4

theorem hasColimitsOfShape_of_isSuccLimit (j : J) (hj : Order.IsSuccLimit j) : HasColimitsOfShape (Set.Iio j) C :=
  HasIterationOfShape.hasColimitsOfShape_of_isSuccLimit j hj

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