English
Differentiability on a set is equivalent to continuity on the set and differentiability in the target-lifted chart for every target chart y.
Русский
Дифференцируемость на множестве эквивалентна непрерывности на множестве и дифференцируемости в целевой карте (для каждой карты y).
LaTeX
$$MDifferentiableOn I I' f s ↔ ContinuousOn f s ∧ ∀ y : M', MDifferentiableOn I 𝓘(𝕜, E') (extChartAt I' y ∘ f) (s ∩ f ⁻¹' (extChartAt I' y).source)$$
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 ⊆ (extChartAt I x).source)
(h2s : MapsTo f s (extChartAt I' y).source) :
MDifferentiableOn I I' f s ↔
DifferentiableOn 𝕜 (extChartAt I' y ∘ f ∘ (extChartAt I x).symm) (extChartAt I x '' s) :=
by
rw [extChartAt_source] at hs h2s
exact mdifferentiableOn_iff_of_mem_maximalAtlas' (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas y) hs h2s
