English
If F creates limits of shape J and D has limits of shape J, then F preserves limits of shape J.
Русский
Если F создаёт пределы формы J, и D имеет пределы формы J, тогда F сохраняет пределы формы J.
LaTeX
$$$[\text{CreatesLimitsOfShape } J F] \wedge [\text{HasLimitsOfShape } J D] \Rightarrow \mathrm{PreservesLimitsOfShape } J F$$$
Lean4
/-- `F` preserves the colimit of shape `J` if it creates these colimits and `D` has them. -/
instance (priority := 100) preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape (F : C ⥤ D)
[CreatesColimitsOfShape J F] [HasColimitsOfShape J D] : PreservesColimitsOfShape J F where
-- see Note [lower instance priority]
