English
If s lies inside a single chart source and f maps s into another chart source, being C^n on s is equivalent to continuity on s and C^n in chart coordinates on extChartAt y.
Русский
Если s вложено в источник одной карты, и f отправляет s в источник другой карты, то C^n на s эквивалентно непрерывности на s и C^n в координатах extChartAt.
LaTeX
$$$ContMDiffOn I I' n f s \;\Longleftrightarrow\; ContinuousOn f s \land ContDiffOn 𝕜 n (extChartAt I' y \circ f \circ (extChartAt I x).symm) (extChartAt I x '' s)$$$
Lean4
/-- If the set where you want `f` to be `C^n` lies entirely in a single chart, and `f` maps it
into a single chart, the fact that `f` is `C^n` on that set can be expressed by purely looking in
these charts.
Note: this lemma uses `extChartAt I x '' s` instead of `(extChartAt I x).symm ⁻¹' s` to ensure
that this set lies in `(extChartAt I x).target`. -/
theorem contMDiffOn_iff_of_subset_source {x : M} {y : M'} (hs : s ⊆ (chartAt H x).source)
(h2s : MapsTo f s (chartAt H' y).source) :
ContMDiffOn I I' n f s ↔
ContinuousOn f s ∧ ContDiffOn 𝕜 n (extChartAt I' y ∘ f ∘ (extChartAt I x).symm) (extChartAt I x '' s) :=
contMDiffOn_iff_of_mem_maximalAtlas (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas y) hs h2s
