English
If hs is UniqueMDiffOn on s, then the target under extChartAt has a unique differential on the intersection with the preimage of s.
Русский
Если hs — UniqueMDiffOn на s, то цель через extChartAt имеет уникальное дифференциальное свойство на пересечении с предобразом s.
LaTeX
$$UniqueMDiffOn.uniqueDiffOn_target_inter$$
Lean4
/-- If a set in a manifold has the unique derivative property, then its pullback by any extended
chart, in the vector space, also has the unique derivative property. -/
theorem uniqueMDiffOn_target_inter (hs : UniqueMDiffOn I s) (x : M) :
UniqueMDiffOn 𝓘(𝕜, E) ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) := by
-- this is just a reformulation of `UniqueMDiffOn.uniqueMDiffOn_preimage`, using as `e`
-- the local chart at `x`.
rw [← PartialEquiv.image_source_inter_eq', inter_comm, extChartAt_source]
exact
(hs.inter (chartAt H x).open_source).image_denseRange' (fun y hy ↦ hasMFDerivWithinAt_extChartAt hy.2) fun y hy ↦
((mdifferentiable_chart _).mfderiv_surjective hy.2).denseRange
