instPreservesWellOrderContinuousOfShapeArrowLeftFuncOfHasIterationOfShape

English

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

Русский

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

LaTeX

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

Lean4

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

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