English
Let x' ∈ M be in the source of the chart at x and f(x') lies in the source of the chart at y. Then f is C^n-differentiable (within the set s at x') if and only if f is continuous within s at x' and, in the chart coordinates, f is C^n-diff on the corresponding domain.
Русский
Пусть x' принадлежит источнику(chartAt H x) и f(x') принадлежит источнику(chartAt H' y). Тогда отображение f является C^n на множестве s в точке x' тогда и только тогда, когда оно непрерывно на s в x' и в координатахchart оно является C^n-дифференцируемым на соответствующей области.
LaTeX
$$$ContMDiffWithinAt I I' n f s x' \;\Longleftrightarrow\; ContinuousWithinAt f s x' \land\quad ContDiffWithinAt 𝕜 n (extChartAt I' y \circ f \circ (extChartAt I x).symm)\;((extChartAt I x).target \cap (extChartAt I x).symm^{-1}(s \cap f^{-1}(extChartAt I' y).source))$$$
Lean4
theorem contMDiffWithinAt_iff_of_mem_source' {x' : M} {y : M'} (hx : x' ∈ (chartAt H x).source)
(hy : f x' ∈ (chartAt H' y).source) :
ContMDiffWithinAt I I' n f s x' ↔
ContinuousWithinAt f s x' ∧
ContDiffWithinAt 𝕜 n (extChartAt I' y ∘ f ∘ (extChartAt I x).symm)
((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
(extChartAt I x x') :=
by
refine (contMDiffWithinAt_iff_of_mem_source hx hy).trans ?_
rw [← extChartAt_source I] at hx
rw [← extChartAt_source I'] at hy
rw [and_congr_right_iff]
set e := extChartAt I x; set e' := extChartAt I' (f x)
refine fun hc => contDiffWithinAt_congr_set ?_
rw [← nhdsWithin_eq_iff_eventuallyEq, ← e.image_source_inter_eq', ← map_extChartAt_nhdsWithin_eq_image' hx, ←
map_extChartAt_nhdsWithin' hx, inter_comm, nhdsWithin_inter_of_mem]
exact hc (extChartAt_source_mem_nhds' hy)