mfderivToContinuousLinearEquiv — Mathlib

English

Every differential of a C^n diffeomorphism is a linear equivalence.

Русский

Каждый дифференциал диффеоморфизма класса C^n является линейной эквивалентностью.

LaTeX

$$$\text{For a } C^n \text{ diffeomorphism } Φ,\; df_x: T_xM \to T_{Φ(x)}N \text{ is a linear isomorphism}$$$

Lean4

/-- Each differential of a `C^n` diffeomorphism of Banach manifolds (`n ≥ 1`)
is a linear equivalence. -/
noncomputable def mfderivToContinuousLinearEquiv (Φ : M ≃ₘ^n⟮I, J⟯ N) (hn : 1 ≤ n) (x : M) :
    TangentSpace I x ≃L[𝕜] TangentSpace J (Φ x) :=
  (Φ.isLocalDiffeomorph x).mfderivToContinuousLinearEquiv hn

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