toDiffeomorph — Mathlib

English

For a fixed n-diffeomorphism h, ContMDiff of h ∘ f equals ContMDiff of f under appropriate coordinates.

Русский

Для данного n-диффеоморфизма h ContMDiff(h ∘ f) равен ContMDiff(f) при соответствующих координатах.

LaTeX

$$ContMDiff I' J m (h ∘ f) ↔ ContMDiff I' I m f$$

Lean4

/-- A continuous linear equivalence between normed spaces is a diffeomorphism. -/
def toDiffeomorph : E ≃ₘ[𝕜] E' where
  contMDiff_toFun := e.contDiff.contMDiff
  contMDiff_invFun := e.symm.contDiff.contMDiff
  toEquiv := e.toLinearEquiv.toEquiv

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