English
A sharper reformulation of C^n within a set at a point, using extended charts, with domain adjusted by chart targets.
Русский
Улучшенная формулировка внутри-набора для $C^n$, с использованием расширенных графов и скорректированных областей.
LaTeX
$$ContMDiffWithinAt I I' n f s x \iff (ContinuousWithinAt f s x) \land ContDiffWithinAt 𝕜 n (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 being `Cⁿ` within a set at a point as continuity within this set at this
point, and being `Cⁿ` in the corresponding extended chart. This form states regularity 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 `contMDiffWithinAt_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 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).target ∩ (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source))
(extChartAt I x x) :=
by
simp only [ContMDiffWithinAt, liftPropWithinAt_iff']
exact and_congr_right fun hc => contDiffWithinAt_congr_set <| hc.extChartAt_symm_preimage_inter_range_eventuallyEq
