preservesLimits_of_natIso — Mathlib

English

If F ≅ G and PreservesLimitsOfSize F, then PreservesLimitsOfSize G.

Русский

Если F ≅ G и PreservesLimitsOfSize F, тогда PreservesLimitsOfSize G.

LaTeX

$$$$\mathrm{Iso}(F,G) \Rightarrow (\mathrm{PreservesLimitsOfSize} F \Rightarrow \mathrm{PreservesLimitsOfSize} G).$$$$

Lean4

/-- Transfer preservation of limits along a natural isomorphism in the functor. -/
theorem preservesLimits_of_natIso {F G : C ⥤ D} (h : F ≅ G) [PreservesLimitsOfSize.{w, w'} F] :
    PreservesLimitsOfSize.{w, w'} G where preservesLimitsOfShape := preservesLimitsOfShape_of_natIso h

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