comp_reflectsLimit — Mathlib

English

If F and G reflect limits of shape J, then F ⋙ G reflects limits of shape J.

Русский

Если F и G отражают пределы формы J, то F ⋙ G отражает пределы формы J.

LaTeX

$$$ [\\text{ReflectsLimitsOfShape } J F] [\\text{ReflectsLimitsOfShape } J G] \\Rightarrow \\text{ReflectsLimitsOfShape } J (F \\cdot G). $$$

Lean4

instance comp_reflectsLimit [ReflectsLimit K F] [ReflectsLimit (K ⋙ F) G] : ReflectsLimit K (F ⋙ G) :=
  ⟨fun h => ReflectsLimit.reflects (isLimitOfReflects G h)⟩

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