English
A variant of the previous differentiability result holds when restricting to a neighborhood in the target model space, showing the robustness of coordinate-change differentiability under extension.
Русский
Вариант предыдущего утверждения для ограниченной окрестности в целевом модельном пространстве демонстрирует устойчивость дифференцируемости перехода координат при расширении.
LaTeX
$$$\\text{ContDiffWithinAt}_{\\mathbb{K}, n} ( f^{\\mathrm{ext}} \\circ (f'.\\mathrm{ext})^{-1}, \\mathrm{range}\\, I, x)$$$
Lean4
theorem contDiffWithinAt_extend_coord_change' [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M)
(hf' : f' ∈ maximalAtlas I n M) {x : M} (hxf : x ∈ f.source) (hxf' : x ∈ f'.source) :
ContDiffWithinAt 𝕜 n (f.extend I ∘ (f'.extend I).symm) (range I) (f'.extend I x) :=
by
refine contDiffWithinAt_extend_coord_change hf hf' ?_
rw [← extend_image_source_inter]
exact mem_image_of_mem _ ⟨hxf', hxf⟩