isStandardSmoothOfRelativeDimension_holdsForLocalizationAway

English

HoldsForLocalizationAway IsStandardSmoothOfRelativeDimension 0.

Русский

HoldsForLocalizationAway IsStandardSmoothOfRelativeDimension 0.

LaTeX

$$$$ \operatorname{HoldsForLocalizationAway}( \operatorname{IsStandardSmoothOfRelativeDimension}(0) ). $$$$

Lean4

theorem isStandardSmoothOfRelativeDimension_holdsForLocalizationAway :
    HoldsForLocalizationAway (IsStandardSmoothOfRelativeDimension 0) :=
  by
  introv R h
  exact IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway r

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