instIsEquivalenceLocalizationLift

English

The Localization.Construction.lift is an equivalence, hence the lifted category is equivalent to the targetLocalization.

Русский

Конструкция подъема локализации lift является эквэлентной, следовательно локализованные категории эквивалентны целевой локализации.

LaTeX

$$$(Localization.Construction.lift L (inverts L W)).IsEquivalence$$$

Lean4

instance : (Localization.Construction.lift L (inverts L W)).IsEquivalence :=
  (inferInstance : L.IsLocalization W).isEquivalence

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