English
Under suitable atlas membership, the local differentiability of the extended coordinate-change map at a point x holds within a range, ensuring local smooth compatibility of chart transitions.
Русский
При условии принадлежности атласа локальная гладкость перехода координат на точке x сохраняется внутри диапазона, обеспечивая локальную гладкость переходов карт.
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 : E} (hx : x ∈ ((f'.extend I).symm ≫ f.extend I).source) :
ContDiffWithinAt 𝕜 n (f.extend I ∘ (f'.extend I).symm) (range I) x :=
by
apply (contDiffOn_extend_coord_change hf hf' x hx).mono_of_mem_nhdsWithin
rw [extend_coord_change_source] at hx ⊢
obtain ⟨z, hz, rfl⟩ := hx
exact I.image_mem_nhdsWithin ((OpenPartialHomeomorph.open_source _).mem_nhds hz)
