English
For a continuous linear equivalence e, UniqueDiffOn 𝕜 (preimage of s under e) iff UniqueDiffOn 𝕜 s.
Русский
Для непрерывной линейной эквивенности e, UniqueDiffOn 𝕜 (предобраз S) эквивалентно UniqueDiffOn 𝕜 S.
LaTeX
$$$$ \\UniqueDiffOn 𝕜 (e^{-1} '' s) \\iff \\UniqueDiffOn 𝕜 s $$$$
Lean4
/-- If a set has the unique differentiability property at a point x, then the image of this set
under a map with onto derivative has also the unique differentiability property at the image point.
-/
theorem uniqueDiffWithinAt (h : HasFDerivWithinAt f f' s x) (hs : UniqueDiffWithinAt 𝕜 s x) (h' : DenseRange f') :
UniqueDiffWithinAt 𝕜 (f '' s) (f x) :=
by
refine ⟨h'.dense_of_mapsTo f'.continuous hs.1 ?_, h.continuousWithinAt.mem_closure_image hs.2⟩
change Submodule.span 𝕜 (tangentConeAt 𝕜 s x) ≤ (Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x))).comap f'
rw [Submodule.span_le]
exact h.mapsTo_tangent_cone.mono Subset.rfl Submodule.subset_span
