English
If a map f is ContMDiffWithinAt of order n on a set s around x, with n ≥ 1, then f is differentiable within s at x.
Русский
Если отображение f гладко внутри области s вокруг точки x в смысле ContMDiffWithinAt порядка n и n ≥ 1, то f дифференцируемо внутри области s в точке x.
LaTeX
$$$ContMDiffWithinAt I I' n f s x \Rightarrow (1 \le n) \rightarrow MDifferentiableWithinAt I I' f s x$$$
Lean4
theorem mdifferentiableWithinAt (hf : ContMDiffWithinAt I I' n f s x) (hn : 1 ≤ n) :
MDifferentiableWithinAt I I' f s x :=
by
suffices h : MDifferentiableWithinAt I I' f (s ∩ f ⁻¹' (extChartAt I' (f x)).source) x
by
rwa [mdifferentiableWithinAt_inter'] at h
apply hf.1.preimage_mem_nhdsWithin
exact extChartAt_source_mem_nhds (f x)
rw [mdifferentiableWithinAt_iff]
exact ⟨hf.1.mono inter_subset_left, (hf.2.differentiableWithinAt (mod_cast hn)).mono (by mfld_set_tac)⟩
