English
If x' lies in the source of the chart at x, then differentiability within a set s at x' is equivalent to differentiability within the model with corners on the translated map.
Русский
Если x' лежит в области определения карты в x, то дифференцируемость внутри s в x' эквивалентна дифференцируемости в расширенной карте.
LaTeX
$$MDifferentiableWithinAt I I' f s x' ↔ MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (extChartAt I x).symm) (range I) (extChartAt I x x')$$
Lean4
theorem mdifferentiableOn_iff_of_mem_maximalAtlas (he : e ∈ maximalAtlas I 1 M) (he' : e' ∈ maximalAtlas I' 1 M')
(hs : s ⊆ e.source) (h2s : MapsTo f s e'.source) :
MDifferentiableOn I I' f s ↔
ContinuousOn f s ∧ DifferentiableOn 𝕜 (e'.extend I' ∘ f ∘ (e.extend I).symm) (e.extend I '' s) :=
by
simp_rw [ContinuousOn, DifferentiableOn, Set.forall_mem_image, ← forall_and, MDifferentiableOn]
exact forall₂_congr fun x hx => mdifferentiableWithinAt_iff_image he he' hs (hs hx) (h2s hx)
