reflectsLimit_of_reflectsLimitsOfShape

English

If F reflects limits of shape J, then ReflectsLimit K F holds for any K.

Русский

Если F отражает предел по форме J, тогда ReflectsLimit K F выполняется для любой K.

LaTeX

$$$ \\text{ReflectsLimitsOfShape } J F \\Rightarrow \\text{ReflectsLimit } K F. $$$

Lean4

instance (priority := 100) reflectsLimit_of_reflectsLimitsOfShape (K : J ⥤ C) (F : C ⥤ D) [ReflectsLimitsOfShape J F] :
    ReflectsLimit K F :=
  ReflectsLimitsOfShape.reflectsLimit

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