mdifferentiableAt_extChartAt — Mathlib

English

The derivative of extChartAt composed with the derivative of the inverse of extChartAt yields the identity map on the tangent spaces.

Русский

Производная extChartAt, скомпонованная с производной обратной extChartAt, даёт тождественное отображение на касательных пространствах.

LaTeX

$$$(mfderiv I \mathcal{I} (\mathrm{extChartAt} I x) ((\mathrm{extChartAt} I x).symm y)) \circ_L (mfderivWithin \mathcal{I} I (\mathrm{extChartAt} I x).symm (range I) y) = \mathrm{ContinuousLinearMap.id}_{\mathrm{TangentSpace} I x}$$$

Lean4

theorem mdifferentiableAt_extChartAt (h : y ∈ (chartAt H x).source) : MDifferentiableAt I 𝓘(𝕜, E) (extChartAt I x) y :=
  (hasMFDerivAt_extChartAt h).mdifferentiableAt

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