contMDiffWithinAt_extChartAt_symm_range_self

English

Let M be a C^n manifold with model I. Then the inverse of the coordinate chart at x, regarded as a map from the model space to M, is C^n on the image of the model I at the point extChartAt I x x.

Русский

Пусть M — C^n многообразие с моделью I. Тогда обратная карта координат в точке x, рассматриваемая как отображение из пространства-модели в M, является C^n на образе модели I в точке extChartAt I x x.

LaTeX

$$$(\\operatorname{extChartAt} I x)^{-1} : \\operatorname{range}(I) \\to M \\quad \\text{is } C^{n} \\text{ at } \\operatorname{extChartAt} I x x.$$$

Lean4

theorem contMDiffWithinAt_extChartAt_symm_range_self (x : M) :
    ContMDiffWithinAt 𝓘(𝕜, E) I n (extChartAt I x).symm (range I) (extChartAt I x x) :=
  (contMDiffWithinAt_extChartAt_symm_target_self x).mono_of_mem_nhdsWithin (extChartAt_target_mem_nhdsWithin x)

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