preservesLimit_of_reflects_of_preserves

English

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

Русский

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

LaTeX

$$$[\\mathrm{PreservesLimitsOfShape}\\,J\\,(F \\;⋙\\; G)] \\land [\\mathrm{ReflectsLimitsOfShape}\\,J\\,G] \\Rightarrow \\mathrm{PreservesLimitsOfShape}\\,J\\,F$$$

Lean4

/-- If `F ⋙ G` preserves limits for `K`, and `G` reflects limits for `K ⋙ F`,
then `F` preserves limits for `K`. -/
theorem preservesLimit_of_reflects_of_preserves [PreservesLimit K (F ⋙ G)] [ReflectsLimit (K ⋙ F) G] :
    PreservesLimit K F :=
  ⟨fun h =>
    ⟨by
      apply isLimitOfReflects G
      apply isLimitOfPreserves (F ⋙ G) h⟩⟩

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