English
The coordinate change map between any two charts is C^n on its source domain; this is the smoothness of the transition maps in the atlas.
Русский
Переход между двумя картами гладкий класса 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 writtenInExtChartAt_chartAt_comp [ChartedSpace H H'] (x : M') {y}
(hy :
y ∈
letI := ChartedSpace.comp H H' M';
(extChartAt I x).target) :
(letI := ChartedSpace.comp H H' M';
writtenInExtChartAt I I x (chartAt H' x) y) =
y :=
by
letI := ChartedSpace.comp H H' M'
simp_all only [mfld_simps, chartAt_comp]