English
If the set where f is to be differentiable lies entirely in a single chart source, differentiability on that set is equivalent to differentiability in the target chart after restriction.
Русский
Если множество, на котором требуется дифференцируемость, целиком лежит в области определения одной карты, то дифференцируемость на этом множестве эквивалентна дифференцируемости в целевой карте после ограничения.
LaTeX
$$MDifferentiableOn I I' f s ↔ ContinuousOn f s ∧ DifferentiableOn 𝕜 (extChartAt I' y ∘ f ∘ (extChartAt I x).symm) (extChartAt I x '' s)$$
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. -/
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).symm ⁻¹' s ∩ range I)
(extChartAt I x x') :=
mdifferentiableWithinAt_iff_of_mem_maximalAtlas (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas y) hx hy
