English
If a set s has the unique differential property, f differentiable on s with MF-derivative f' of dense range, then f''s has the unique differential property.
Русский
Если множество s обладает уникальным дифференциалом, функция f дифференцируема на s с MF-деривативом f' и плотным образом образующая плотность, то образ f '' s имеет уникальное дифференциальное свойство.
LaTeX
$$$UniqueMDiffOn\\ I' (f '' s)\\text{ under dense range condition}$$$
Lean4
/-- If `s` has the unique differential property at `x`, `f` is differentiable within `s` at `x` and
its derivative has dense range, then `f '' s` has the unique differential property at `f x`. -/
theorem image_denseRange (hs : UniqueMDiffWithinAt I s x) {f : M → M'} {f' : E →L[𝕜] E'}
(hf : HasMFDerivWithinAt I I' f s x f') (hd : DenseRange f') : UniqueMDiffWithinAt I' (f '' s) (f x) := by
/- Rewrite in coordinates, apply `HasFDerivWithinAt.uniqueDiffWithinAt`. -/
have := hs.inter' <| hf.1 (extChartAt_source_mem_nhds (I := I') (f x))
refine (((hf.2.mono ?sub1).uniqueDiffWithinAt this hd).mono ?sub2).congr_pt ?pt
case pt => simp only [mfld_simps]
case sub1 => mfld_set_tac
case sub2 =>
rintro _ ⟨y, ⟨⟨hys, hfy⟩, -⟩, rfl⟩
exact ⟨⟨_, hys, ((extChartAt I' (f x)).left_inv hfy).symm⟩, mem_range_self _⟩
