mfderivToContinuousLinearEquiv_coe

English

The differential map at x is a continuous linear equivalence between tangent spaces.

Русский

Дифференциал в точке x образует непрерывное линейное биективное преобразование между касательными пространствами.

LaTeX

$$$df_x: T_xM \cong T_{f(x)}N$ is a continuous linear equivalence$$

Lean4

theorem mfderivToContinuousLinearEquiv_coe (Φ : M ≃ₘ^n⟮I, J⟯ N) (hn : 1 ≤ n) :
    Φ.mfderivToContinuousLinearEquiv hn x = mfderiv I J Φ x := by rfl

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