isStandardSmoothOfRelativeDimension_localizationPreserves

English

Localization preserves IsStandardSmoothOfRelativeDimension n.

Русский

Локализация сохраняет IsStandardSmoothOfRelativeDimension n.

LaTeX

$$$$ \operatorname{LocalizationPreserves} \bigl( \operatorname{IsStandardSmoothOfRelativeDimension}(n) \bigr). $$$$

Lean4

theorem isStandardSmoothOfRelativeDimension_localizationPreserves :
    LocalizationPreserves (IsStandardSmoothOfRelativeDimension n) :=
  (isStandardSmoothOfRelativeDimension_isStableUnderBaseChange n).localizationPreserves

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