English
If F and G both preserve well-order continuous of shape J, then F ⋙ G preserves well-order continuous of shape J.
Русский
Если F и G оба сохраняют WellOrderContinuousOfShape J, то F ⋙ G сохраняет WellOrderContinuousOfShape J.
LaTeX
$$$\text{PreservesWellOrderContinuousOfShape } J (F \circ G)$$$
Lean4
instance (F : J ⥤ C) (G : C ⥤ D) [F.IsWellOrderContinuous] [PreservesWellOrderContinuousOfShape J G] :
(F ⋙ G).IsWellOrderContinuous where
nonempty_isColimit j
hj :=
⟨by
have := preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape G j hj
exact isColimitOfPreserves G (F.isColimitOfIsWellOrderContinuous j hj)⟩
