English
Continuing in the target chart formulation, a map f is MDifferentiable if and only if it is continuous and, for every chart y in the target, the composition extChartAt I' y ∘ f is differentiable on the preimage of the chart’s source in the target coordinates.
Русский
Продолжая в терминах целевой карты, отображение f дифференцируемо по картам, если и только если оно непрерывно, и для каждой карты y в целевом пространстве композиция extChartAt I' y ∘ f дифференцируема на предобразе области источника карты в целевых координатах.
LaTeX
$$$MDifferentiable I I' f \iff ( Continuous f \wedge \forall y: M',\, MDifferentiableOn I 𝓘(𝕜, E') (extChartAt I' y \circ f) (f^{-1}(extChartAt I' y).source) )$$$
Lean4
/-- One can reformulate smoothness as continuity and smoothness in any extended chart in the
target. -/
theorem mdifferentiable_iff_target :
MDifferentiable I I' f ↔
Continuous f ∧ ∀ y : M', MDifferentiableOn I 𝓘(𝕜, E') (extChartAt I' y ∘ f) (f ⁻¹' (extChartAt I' y).source) :=
by
rw [← mdifferentiableOn_univ, mdifferentiableOn_iff_target]
simp [continuousOn_univ]
