English
If there exist charts e and e' from the maximal atlas around x and f x, and s is contained in the source of e and maps into the source of e', then differentiability on s is equivalent to differentiability in the extended charts on the image of s.
Русский
Если существуют карты e и e' из максимального атласа вокруг x и f(x), и s вложено в область определения e и переходит в область определения e', то дифференцируемость на s эквивалентна дифференцируемости в расширенных картах на образе s.
LaTeX
$$MDifferentiableWithinAt I I' f s x ↔ ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 (e'.extend I' ∘ f ∘ (e.extend I).symm) ((e.extend I).symm ⁻¹' s ∩ range I) (e.extend I x)$$
Lean4
theorem mdifferentiableAt_iff_target_of_mem_source [IsManifold I' 1 M'] {x : M} {y : M'}
(hy : f x ∈ (chartAt H' y).source) :
MDifferentiableAt I I' f x ↔ ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') (extChartAt I' y ∘ f) x := by
rw [← mdifferentiableWithinAt_univ, mdifferentiableWithinAt_iff_target_of_mem_source hy, continuousWithinAt_univ, ←
mdifferentiableWithinAt_univ]
