instIsStableUnderTransfiniteCompositionOfShapeOfIsMultiplicativeOfRespectsIsoOfIsStableUnderFilteredColimits

English

The operation W ↦ W.transfiniteCompositionsOfShape J is monotone in W.

Русский

Операция W ↦ W.transfiniteCompositionsOfShape J монотонна по отношению к W.

LaTeX

$$$W_1 \\le W_2 \\implies W_1.transfiniteCompositionsOfShape J \\le W_2.transfiniteCompositionsOfShape J$$$

Lean4

instance [W.IsMultiplicative] [W.RespectsIso] [MorphismProperty.IsStableUnderFilteredColimits.{w, w} W] :
    W.IsStableUnderTransfiniteCompositionOfShape J :=
  .of_isStableUnderColimitsOfShape (fun _ _ _ _ _ ↦ by infer_instance)

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