English
If the chart e at x and the chart e' at y belong to maximal atlases of I and I' at level n, and s is contained in e.source with f sending s into e'.source, then being C^n on s is equivalent to being continuous on s and C^n in the chart coordinates on e'' and f behind the scenes.
Русский
Если указываются карты e и e', принадлежащие к максимальным атласам манипуляции I и I' на уровне n, при этом s ⊆ e.source и MapsTo f s e'.source, то ContMDiffOn I I' n f s эквивалентно ContinuousOn f s и ContDiffOn 𝕜 n в координатах карт.
LaTeX
$$$ContMDiffOn I I' n f s \;\Longleftrightarrow\; ContinuousOn f s \land\\quad ContDiffOn 𝕜 n (e'.extend I' \circ f \circ (e.extend I)^{-1}) (e \!\!\!\!\!\!\!\!\!\!\!\!\!\!\! s) $$$
Lean4
theorem contMDiffOn_iff_of_mem_maximalAtlas (he : e ∈ maximalAtlas I n M) (he' : e' ∈ maximalAtlas I' n M')
(hs : s ⊆ e.source) (h2s : MapsTo f s e'.source) :
ContMDiffOn I I' n f s ↔
ContinuousOn f s ∧ ContDiffOn 𝕜 n (e'.extend I' ∘ f ∘ (e.extend I).symm) (e.extend I '' s) :=
by
simp_rw [ContinuousOn, ContDiffOn, Set.forall_mem_image, ← forall_and, ContMDiffOn]
exact forall₂_congr fun x hx => contMDiffWithinAt_iff_image he he' hs (hs hx) (h2s hx)
