English
If f x lies in the source of a target chart, differentiability within a set s at x is equivalent to continuity of f on s at x and chart-differentiability in the target chart around f x.
Русский
Если f x лежит в области определения целевой карты, то дифференцируемость внутри s в x эквивалентна непрерывности f на s в x и дифференцируемости в целевой карте вокруг f x.
LaTeX
$$MDifferentiableWithinAt I I' f s x ↔ ContinuousWithinAt f s x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') (extChartAt I' (f x) ∘ f) s x$$
Lean4
/-- One can reformulate smoothness within a set at a point as continuity within this set at this
point, and smoothness in any chart containing that point. Version requiring differentiability
in the target instead of `range I`. -/
theorem mdifferentiableWithinAt_iff_of_mem_source' {x' : M} {y : M'} (hx : x' ∈ (chartAt H x).source)
(hy : f x' ∈ (chartAt H' y).source) :
MDifferentiableWithinAt I I' f s x' ↔
ContinuousWithinAt f s x' ∧
DifferentiableWithinAt 𝕜 (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 (mdifferentiableWithinAt_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 => differentiableWithinAt_congr_nhds ?_
rw [← 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)
