English
Differentiability on a set is equivalent to differentiability in extended charts on the image of the set under the atlas charts.
Русский
Дифференцируемость на множестве эквивалентна дифференцируемости в расширенных картах на образ множества через карты атласа.
LaTeX
$$MDifferentiableOn I I' f s ↔ ContinuousOn f s ∧ DifferentiableOn 𝕜 (Function.comp (e'.extend I').toFun (Function.comp f (e.extend I).symm.toFun)) (Set.image (e.extend I).toFun s)$$
Lean4
/-- An alternative formulation of `mdifferentiableWithinAt_iff_of_mem_maximalAtlas`
if the set if `s` lies in `e.source`. -/
theorem mdifferentiableWithinAt_iff_image {x : M} (he : e ∈ maximalAtlas I 1 M) (he' : e' ∈ maximalAtlas I' 1 M')
(hs : s ⊆ e.source) (hx : x ∈ e.source) (hy : f x ∈ e'.source) :
MDifferentiableWithinAt I I' f s x ↔
ContinuousWithinAt f s x ∧
DifferentiableWithinAt 𝕜 (e'.extend I' ∘ f ∘ (e.extend I).symm) (e.extend I '' s) (e.extend I x) :=
by
rw [mdifferentiableWithinAt_iff_of_mem_maximalAtlas he he' hx hy, and_congr_right_iff]
refine fun _ => differentiableWithinAt_congr_nhds ?_
simp_rw [nhdsWithin_eq_iff_eventuallyEq, e.extend_symm_preimage_inter_range_eventuallyEq hs hx]
