instPreservesWellOrderContinuousOfShapeFunctorObjEvaluationOfHasIterationOfShape

English

If G preserves well-order continuous of shape J, then G preserves shape (Iio j) colimits for a given j with IsSuccLimit.

Русский

Если G сохраняет WellOrderContinuousOfShape J, тогда G сохраняет колимиты формы Set.Iio j для заданного j, когда hj является IsSuccLimit.

LaTeX

$$$\text{PreservesColimitsOfShape}(\text{Set.Iio } j)\, G$$$

Lean4

instance [HasIterationOfShape J C] (K : Type*) [Category K] (X : K) :
    PreservesWellOrderContinuousOfShape J ((evaluation K C).obj X) where
  preservesColimitsOfShape j
    hj := by
    have := hasColimitsOfShape_of_isSuccLimit C j hj
    infer_instance

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