English
The differential of the extended chart at a point y in the source of extChartAt I x is invertible; in other words, the extended chart is locally a diffeomorphism at that point.
Русский
Дифференциал расширенного чарта в точке y из области определения extChartAt I x является обратимым линейным отображением; следовательно, расширённый чарт вокруг этой точки задаёт локальный диффеоморфизм.
LaTeX
$$$\bigl( \operatorname{mfderiv} I \; \mathcal{I}(\mathbb{k},E) \; (\operatorname{extChartAt} I x) \; y \bigr) \text{ is a linear isomorphism }$$$
Lean4
theorem isInvertible_mfderiv_extChartAt {y : M} (hy : y ∈ (extChartAt I x).source) :
(mfderiv I 𝓘(𝕜, E) (extChartAt I x) y).IsInvertible :=
by
have h'y : extChartAt I x y ∈ (extChartAt I x).target := (extChartAt I x).map_source hy
have Z :=
ContinuousLinearMap.IsInvertible.of_inverse (mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm h'y)
(mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt h'y)
have : (extChartAt I x).symm ((extChartAt I x) y) = y := (extChartAt I x).left_inv hy
rwa [this] at Z
