English
If hs is UniqueMDiffOn on s, then the target under extChartAt has unique differential on the intersection with 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 uniqueDiffOn_target_inter (hs : UniqueMDiffOn I s) (x : M) :
UniqueDiffOn 𝕜 ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) :=
(hs.uniqueMDiffOn_target_inter x).uniqueDiffOn