instPreservesWellOrderContinuousOfShapeArrowRightFuncOfHasIterationOfShape

English

If HasIterationOfShape J C holds, then Arrow.rightFunc preserves well-order continuous of shape J.

Русский

Если существует HasIterationOfShape J C, то Arrow.rightFunc сохраняет WellOrderContinuousOfShape J.

LaTeX

$$$\text{PreservesWellOrderContinuousOfShape } J (\text{Arrow.rightFunc})$$$

Lean4

instance [HasIterationOfShape J C] : PreservesWellOrderContinuousOfShape J (Arrow.rightFunc : _ ⥤ C) where
  preservesColimitsOfShape j
    hj := by
    have := hasColimitsOfShape_of_isSuccLimit C j hj
    infer_instance

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