isStandardSmoothOfRelativeDimension_respectsIso

English

RespectsIso for IsStandardSmoothOfRelativeDimension n: standard-smoothness at relative dimension n is preserved under isomorphisms.

Русский

Изоморфизмы сохраняют стандартную гладкость относительно размерности n для IsStandardSmoothOfRelativeDimension.

LaTeX

$$$$ \operatorname{RespectsIso}(\operatorname{IsStandardSmoothOfRelativeDimension}(n)). $$$$

Lean4

theorem isStandardSmoothOfRelativeDimension_respectsIso : RespectsIso (@IsStandardSmoothOfRelativeDimension n)
    where
  left {R S T _ _ _} f e
    hf := by
    rw [← zero_add n]
    exact (IsStandardSmoothOfRelativeDimension.equiv e).comp hf
  right {R S T _ _ _} f e
    hf := by
    rw [← add_zero n]
    exact hf.comp (IsStandardSmoothOfRelativeDimension.equiv e)

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