English
A variant reformulation: differentiability within a set s at x is equivalent to continuity within s at x and differentiability in the chart after a prime modification of the target intersection.
Русский
Вариант переформулирования: дифференцируемость внутри множества s в точке x эквивалентна непрерывности внутри s в точке x и дифференцируемости в карте после модификации целевого пересечения (с апострофом).
LaTeX
$$MDifferentiableWithinAt I I' f s x ↔ ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 (extChartAt I' (f x) ∘ f ∘ (extChartAt I x).symm) ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)) (extChartAt I x x)$$
Lean4
/-- One can reformulate smoothness within a set at a point as continuity within this set at this
point, and smoothness in the corresponding extended chart. -/
theorem mdifferentiableWithinAt_iff :
MDifferentiableWithinAt I I' f s x ↔
ContinuousWithinAt f s x ∧
DifferentiableWithinAt 𝕜 (extChartAt I' (f x) ∘ f ∘ (extChartAt I x).symm)
((extChartAt I x).symm ⁻¹' s ∩ range I) (extChartAt I x x) :=
by simp_rw [MDifferentiableWithinAt, ChartedSpace.liftPropWithinAt_iff']; rfl
