English
A variant stating the equivalence for ContMDiffOn when s is contained in (extChartAt x).source with respect to subset properties.
Русский
Альтернатива, говорящая об эквивалентности ContMDiffOn, когда s ⊆ (extChartAt x).source.
LaTeX
$$$ContMDiffOn I I' n f s \;\Longleftrightarrow\; 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 ⊆ (extChartAt I x).source)
(h2s : MapsTo f s (extChartAt I' y).source) :
ContMDiffOn I I' n f s ↔ ContDiffOn 𝕜 n (extChartAt I' y ∘ f ∘ (extChartAt I x).symm) (extChartAt I x '' s) :=
by
rw [extChartAt_source] at hs h2s
exact contMDiffOn_iff_of_mem_maximalAtlas' (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas y) hs h2s
