English
For a point x' in the source of the chart at x and f(x') in the source of the chart at y, being differentiable of order n at x' is equivalent to f being continuous at x' and being C^n in chart coordinates at x and y.
Русский
Пусть x' лежит в источнике chartAt H x и f(x') лежит в источнике chartAt H' y. Тогда ContMDiffAt I I' n f x' эквивалентно непрерывности f в x' и тому, что в координатах через extChartAt I x и extChartAt I' y функция является C^n на соответствующей области.
LaTeX
$$$ContMDiffAt I I' n f x' \;\Longleftrightarrow\; (ContinuousAt f x') \,\land\\quad ContDiffWithinAt 𝕜 n (extChartAt I' y \circ f \circ (extChartAt I x).symm)\; (\text{range } I) \;(extChartAt I x x')$$$
Lean4
theorem contMDiffAt_iff_of_mem_source {x' : M} {y : M'} (hx : x' ∈ (chartAt H x).source)
(hy : f x' ∈ (chartAt H' y).source) :
ContMDiffAt I I' n f x' ↔
ContinuousAt f x' ∧
ContDiffWithinAt 𝕜 n (extChartAt I' y ∘ f ∘ (extChartAt I x).symm) (range I) (extChartAt I x x') :=
(contMDiffWithinAt_iff_of_mem_source hx hy).trans <| by rw [continuousWithinAt_univ, preimage_univ, univ_inter]