stableUnderCompositionWithLocalizationAway

English

If a property P is stable under composition and holds for localization away, then it remains stable under localization away for composed maps.

Русский

Если свойство P устойчиво к композиции и сохраняется при локализации по away, то сохраняется и при композициях локализаций.

LaTeX

$$$(\\text{StableUnderComposition }P) \\land (\\text{HoldsForLocalizationAway }P) \\Rightarrow (\\text{StableUnderCompositionWithLocalizationAway }P)$$$

Lean4

theorem stableUnderCompositionWithLocalizationAway (hPc : RingHom.StableUnderComposition P)
    (hPl : HoldsForLocalizationAway P) : StableUnderCompositionWithLocalizationAway P :=
  by
  constructor
  · introv _ _ hf
    exact hPc _ _ (hPl S r) hf
  · introv _ _ hf
    exact hPc _ _ hf (hPl T s)

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