hasIterationOfShape_of_initialSeg

English

If J is linear order with SuccOrder and WellFoundedLT, and α is initialSeg of a relation with a nonempty type, then HasIterationOfShape α C.

Русский

Пусть J — линейный порядок с SuccOrder и WellFoundedLT, и α — начальный сегмент относительно отношения; тогда HasIterationOfShape α C.

LaTeX

$$$\mathrm{HasIterationOfShape}(\alpha, C)$$$

Lean4

theorem hasIterationOfShape_of_initialSeg {α : Type*} [LinearOrder α] (h : α ≤i J) [Nonempty α] :
    HasIterationOfShape α C
    where
  hasColimitsOfShape := hasColimitsOfShape_of_initialSeg C h
  hasColimitsOfShape_of_isSuccLimit j
    hj := by
    have := hj.nonempty_Iio.to_subtype
    exact hasColimitsOfShape_of_initialSeg _ (InitialSeg.trans (Set.principalSegIio j) h)

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