English
If s lies within a chart source and f maps s into a chart source, the C^n equivalence reduces to chart-based diffeomorphism.
Русский
Если s лежит внутри источника карты и f отображает s в источник карты, то эквивалентность C^n сводится к диффеоморфизму в координатах карты.
LaTeX
$$$ContMDiffOn I I' n f s \;\Longleftrightarrow\; ContinuousOn f s ∧ ContDiffOn 𝕜 n (e'.extend I' \circ f \circ (e.extend I).symm) (e.extend I '' s)$$$
Lean4
/-- One can reformulate being `C^n` as continuity and being `C^n` in any extended chart. -/
theorem contMDiff_iff :
ContMDiff I I' n f ↔
Continuous f ∧
∀ (x : M) (y : M'),
ContDiffOn 𝕜 n (extChartAt I' y ∘ f ∘ (extChartAt I x).symm)
((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' (f ⁻¹' (extChartAt I' y).source)) :=
by simp [← contMDiffOn_univ, contMDiffOn_iff, continuousOn_univ]
