mfderivToContinuousLinearEquiv — Mathlib

English

The mfderiv map coincides with the standard differential mfderiv I J f x.

Русский

Коэффициент mfderiv совпадает с обычным дифференциалом mfderiv I J f x.

LaTeX

$$$(hf.mfderivToContinuousLinearEquiv hn x) = mfderiv I J f x$$$

Lean4

/-- If `f` is a `C^n` local diffeomorphism of Banach manifolds (`n ≥ 1`),
each differential is a linear equivalence. -/
noncomputable def mfderivToContinuousLinearEquiv (hf : IsLocalDiffeomorph I J n f) (hn : 1 ≤ n) (x : M) :
    TangentSpace I x ≃L[𝕜] TangentSpace J (f x) :=
  (hf x).mfderivToContinuousLinearEquiv hn

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