contDiffWithinAt_ext_coord_change

English

In a manifold setting, the coordinate change map between two extended charts is C^n on its natural domain.

Русский

В условии многообразия переход между двумя расширенными картами гладкий класса C^n на своей естественной области определения.

LaTeX

$$$\text{ContDiffOn}_{\mathbb{K}}^n(\mathrm{extChartAt} I x \circ (\mathrm{extChartAt} I x').symm) ((\mathrm{extChartAt} I x').symm \circ \mathrm{extChartAt} I x).\text{source}$$$

Lean4

theorem contDiffWithinAt_ext_coord_change [IsManifold I n M] (x x' : M) {y : E}
    (hy : y ∈ ((extChartAt I x').symm ≫ extChartAt I x).source) :
    ContDiffWithinAt 𝕜 n (extChartAt I x ∘ (extChartAt I x').symm) (range I) y :=
  contDiffWithinAt_extend_coord_change (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas x') hy

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