English
A reformulation of differentiability within a set at a point as continuity within the set at the point and differentiability in the corresponding lifted chart.
Русский
Переопределение дифференцируемости внутри множества в точке как непрерывности внутри множества в точке и дифференцируемости в соответствующей лазерной карте.
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. This form states smoothness of `f`
written in such a way that the set is restricted to lie within the domain/codomain of the
corresponding charts.
Even though this expression is more complicated than the one in `mdifferentiableWithinAt_iff`, it is
a smaller set, but their germs at `extChartAt I x x` are equal. It is sometimes useful to rewrite
using this in the goal.
-/
theorem mdifferentiableWithinAt_iff_target_inter' :
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) :=
by
simp only [MDifferentiableWithinAt, liftPropWithinAt_iff']
exact
and_congr_right fun hc => differentiableWithinAt_congr_nhds <| hc.nhdsWithin_extChartAt_symm_preimage_inter_range
