English
Being C^n in a set at a point is equivalent to continuity at that point in the set together with being C^n in the chart expression.
Русский
Бытие $C^n$ внутри множества в точке эквивалентно непрерывности в этой точке на множестве и $C^n$ в выражении через графы.
LaTeX
$$ContMDiffWithinAt I I' n f s x \leftrightarrow (ContinuousWithinAt f s x) \land (ContDiffWithinAt 𝕜 n (extChartAt I' (f x) ∘ f ∘ (extChartAt I x).symm) ((extChartAt I x).symm ⁻¹' s ∩ range I) (extChartAt I x x))$$
Lean4
/-- One can reformulate being `C^n` within a set at a point as continuity within this set at this
point, and being `C^n` in the corresponding extended chart. -/
theorem contMDiffWithinAt_iff :
ContMDiffWithinAt I I' n f s x ↔
ContinuousWithinAt f s x ∧
ContDiffWithinAt 𝕜 n (extChartAt I' (f x) ∘ f ∘ (extChartAt I x).symm) ((extChartAt I x).symm ⁻¹' s ∩ range I)
(extChartAt I x x) :=
by simp_rw [ContMDiffWithinAt, liftPropWithinAt_iff']; rfl
