instPreservesWellOrderContinuousOfShapeComp

English

If J is a linear order and HasIterationOfShape J C holds, then Arrow.leftFunc preserves well-order continuity of shape J.

Русский

Если J линейный порядок и HasIterationOfShape J C, тогда Arrow.leftFunc сохраняет WellOrderContinuousOfShape J.

LaTeX

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

Lean4

instance (G₁ : C ⥤ D) (G₂ : D ⥤ E) [PreservesWellOrderContinuousOfShape J G₁]
    [PreservesWellOrderContinuousOfShape J G₂] : PreservesWellOrderContinuousOfShape J (G₁ ⋙ G₂) where
  preservesColimitsOfShape j
    hj := by
    have := preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape G₁ j hj
    have := preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape G₂ j hj
    infer_instance

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