English
If I is a ModelWithCorners and x, x' ∈ M, then the coordinate change map extChartAt I x ∘ (extChartAt I x').symm is C^n on its domain, i.e., contDiffOn holds on the source of the transition map.
Русский
Если I — модель с углами и x, x' ∈ M, то переходная карта между картами является гладкой класса 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 contDiffOn_ext_coord_change [IsManifold I n M] (x x' : M) :
ContDiffOn 𝕜 n (extChartAt I x ∘ (extChartAt I x').symm) ((extChartAt I x').symm ≫ extChartAt I x).source :=
contDiffOn_extend_coord_change (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas x')
