English
If x is in the source of the chart e in the maximal atlas and y in the target chart, then differentiability within s at x corresponds to differentiability in the appropriate extended chart system.
Русский
Если x принадлежит области определения карты e в максимальном атласе, и y — в целевой карте, то дифференцируемость внутри s в x соответствует дифференцируемости в соответствующей системе расширенных карт.
LaTeX
$$MDifferentiableWithinAt I I' f s x ↔ ContinuousWithinAt f s x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') (extChartAt I' (f x) ∘ f) (s ∩ f⁻¹' (extChartAt I' (f x)).source)$$
Lean4
theorem mdifferentiableWithinAt_iff_source_of_mem_source [IsManifold I 1 M] {x' : M} (hx' : x' ∈ (chartAt H x).source) :
MDifferentiableWithinAt I I' f s x' ↔
MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (extChartAt I x).symm) ((extChartAt I x).symm ⁻¹' s ∩ range I)
(extChartAt I x x') :=
mdifferentiableWithinAt_iff_source_of_mem_maximalAtlas (chart_mem_maximalAtlas x) hx'
