English
Let f be a map between manifolds with corners I and I'. Then f is MDifferentiable if and only if it is continuous and, for every point x in M and every chart y in M', the local coordinate expression of f, given by extChartAt I' y ∘ f ∘ (extChartAt I x)⁻¹, is differentiable on the appropriate domain.
Русский
Пусть f : M → M' между многообразиями с краями имеет структуры I и I'. Тогда f является MDifferentiable тогда и только тогда, когда она непрерывна и для каждой точки x ∈ M и каждой карты y в M' локальное выражение координат extChartAt I' y ∘ f ∘ (extChartAt I x)⁻¹ дифференцируемо на соответствующей области.
LaTeX
$$$MDifferentiable I I' f \iff ( Continuous f \wedge \forall x: M, \forall y: M', \, DifferentiableOn 𝕜 (extChartAt I' y \circ f \circ (extChartAt I x)^{-1})\left((extChartAt I x).target \cap (extChartAt I x)^{-1}\left(f^{-1}((extChartAt I' y).source)\right)\right) )$$$
Lean4
/-- One can reformulate smoothness as continuity and smoothness in any extended chart. -/
theorem mdifferentiable_iff :
MDifferentiable I I' f ↔
Continuous f ∧
∀ (x : M) (y : M'),
DifferentiableOn 𝕜 (extChartAt I' y ∘ f ∘ (extChartAt I x).symm)
((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' (f ⁻¹' (extChartAt I' y).source)) :=
by simp [← mdifferentiableOn_univ, mdifferentiableOn_iff, continuousOn_univ]
