English
If hs is UniqueMDiffOn s and there exists a local diffeomorphism e with MDifferentiable, then UniqueMDiffOn on the pullback under e.
Русский
Если hs является UniqueMDiffOn s и существует локальный диффеоморфизм e с MDifferentiable, то UniqueMDiffOn сохраняется на вытяжке по e.
LaTeX
$$UniqueMDiffOn.uniqueMDiffOn_preimage$$
Lean4
/-- If a set has the unique differential property, then its image under a local
diffeomorphism also has the unique differential property. -/
theorem uniqueMDiffOn_preimage (hs : UniqueMDiffOn I s) {e : OpenPartialHomeomorph M M'} (he : e.MDifferentiable I I') :
UniqueMDiffOn I' (e.target ∩ e.symm ⁻¹' s) := fun _x hx ↦
e.right_inv hx.1 ▸ (hs _ hx.2).preimage_openPartialHomeomorph he (e.map_target hx.1)