English
Reformulates C^n-differentiability as continuity plus chart-diffeomorphism properties targeting charts in the codomain.
Русский
Переопределение C^n-дифференцируемости как непрерывности плюс свойства диффеоморфизм по картам в целевом пространстве.
LaTeX
$$$ContMDiffOn I I' n f s \;\Longleftrightarrow\; ContinuousOn f s ∧ \forall y, ContMDiffOn I 𝓘(𝕜, E') n (extChartAt I' y \circ f) (s \cap f^{-1}(extChartAt I' y).source)$$$
Lean4
/-- One can reformulate being `C^n` as continuity and being `C^n` in any extended chart in the
target. -/
theorem contMDiff_iff_target :
ContMDiff I I' n f ↔
Continuous f ∧ ∀ y : M', ContMDiffOn I 𝓘(𝕜, E') n (extChartAt I' y ∘ f) (f ⁻¹' (extChartAt I' y).source) :=
by
rw [← contMDiffOn_univ, contMDiffOn_iff_target]
simp [continuousOn_univ]
