locally_StableUnderCompositionWithLocalizationAwaySource

English

If P is stable under composition with localization-away maps on the left, then Locally P is stable under such composition on the left as well.

Русский

Если P устойчива к композиции слева сAway, то Locally P устойчива слева.

LaTeX

$$$\operatorname{StableUnderCompositionWithLocalizationAwaySource}(P) \Rightarrow \operatorname{StableUnderCompositionWithLocalizationAwaySource}(\Locally P).$$$

Lean4

/-- If `P` is stable under composition with localization away maps on the left,
then so is `Locally P`. -/
theorem locally_StableUnderCompositionWithLocalizationAwaySource
    (hPa : StableUnderCompositionWithLocalizationAwaySource P) :
    StableUnderCompositionWithLocalizationAwaySource (Locally P) :=
  by
  intro R S T _ _ _ _ r _ f ⟨s, hsone, hs⟩
  refine ⟨s, hsone, fun t ht ↦ ?_⟩
  rw [← comp_assoc]
  exact hPa _ r _ (hs t ht)

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