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