English
Equivalence of differentiability within a set at x with continuity and chart-differentiability measured in the target intersection after lifting.
Русский
Эквивалентность дифференцируемости внутри множества в точке x через непрерывность и дифференцируемость в карте после лифта на пересечении целевых множеств.
LaTeX
$$MDifferentiableWithinAt I I' f s x ↔ ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) (extChartAt I x x)$$
Lean4
theorem mdifferentiableAt_iff_source_of_mem_source [IsManifold I 1 M] {x' : M} (hx' : x' ∈ (chartAt H x).source) :
MDifferentiableAt I I' f x' ↔
MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (extChartAt I x).symm) (range I) (extChartAt I x x') :=
by
simp_rw [← mdifferentiableWithinAt_univ, mdifferentiableWithinAt_iff_source_of_mem_source hx', preimage_univ,
univ_inter]
