English
If the image under f of x lies in the source of the target chart, differentiability within a set s at x is equivalent to continuity on s and chart-differentiability with the target map.
Русский
Если образ f(x) лежит в области определения целевой карты, то дифференцируемость внутри s в x эквивалентна непрерывности на s и дифференцируемости в целевой карте.
LaTeX
$$mdifferentiableWithinAt_iff_target_of_mem_source [IsManifold I' 1 M'] {x : M} {y : M'} (hy : f x ∈ (chartAt H' y).source) : MDifferentiableWithinAt I I' f s x ↔ ContinuousWithinAt f s x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') (extChartAt I' y ∘ f) (s ∩ f ⁻¹' (extChartAt I' y).source) (extChartAt I x x)$$
Lean4
/-- If the set where you want `f` to be smooth lies entirely in a single chart, and `f` maps it
into a single chart, the smoothness of `f` on that set can be expressed by purely looking in
these charts.
Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure
that this set lies in `(extChartAt I x).target`. -/
theorem mdifferentiableOn_iff_of_subset_source {x : M} {y : M'} (hs : s ⊆ (chartAt H x).source)
(h2s : MapsTo f s (chartAt H' y).source) :
MDifferentiableOn I I' f s ↔
ContinuousOn f s ∧ DifferentiableOn 𝕜 (extChartAt I' y ∘ f ∘ (extChartAt I x).symm) (extChartAt I x '' s) :=
mdifferentiableOn_iff_of_mem_maximalAtlas (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas y) hs h2s
