preservesLimits_of_reflects_of_preserves

English

If F ⋙ G preserves limits and G reflects limits, then F preserves limits.

Русский

Если F ⋙ G сохраняет пределы, и G отражает пределы, то F сохраняет пределы.

LaTeX

$$$[\\mathrm{PreservesLimitsOfSize}\\,(F \\;⋙\\; G)] \\land [\\mathrm{ReflectsLimitsOfSize}\\,G] \\Rightarrow \\mathrm{PreservesLimitsOfSize}\\,F$$$

Lean4

/-- If `F ⋙ G` preserves limits and `G` reflects limits, then `F` preserves limits. -/
theorem preservesLimits_of_reflects_of_preserves [PreservesLimitsOfSize.{w', w} (F ⋙ G)]
    [ReflectsLimitsOfSize.{w', w} G] : PreservesLimitsOfSize.{w', w} F where
  preservesLimitsOfShape := preservesLimitsOfShape_of_reflects_of_preserves F G

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