English
If two charts f and f' belong to a maximal atlas, then the coordinate-change map between their extensions is differentiable on their common source. This shows smooth compatibility of the atlas with extensions.
Русский
Если карты f и f' входят в максимальный атлас, то переход координат между их продолжениями гладок на общей области определения. Это демонстрирует гладкую совместимость атласа и расширений.
LaTeX
$$$\\mathrm{ContDiffOn}_{\\mathbb{K}, n}\\big( f^{\\mathrm{ext}} \\circ (f'.\\mathrm{ext})^{-1}, \\mathrm{source} \\big)$$$
Lean4
theorem contDiffOn_extend_coord_change [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M)
(hf' : f' ∈ maximalAtlas I n M) :
ContDiffOn 𝕜 n (f.extend I ∘ (f'.extend I).symm) ((f'.extend I).symm ≫ f.extend I).source :=
by
rw [extend_coord_change_source, I.image_eq]
exact (StructureGroupoid.compatible_of_mem_maximalAtlas hf' hf).1