English
If the subset lies in the source of a chart, differentiability on that subset is equivalent to differentiability in the charted coordinates after applying the chart extension.
Русский
Если множество лежит в области определения карты, то дифференцируемость на этом множестве эквивалентна дифференцируемости в координатах карты после применения её расширения.
LaTeX
$$MDifferentiableOn I I' f s ↔ DifferentiableOn 𝕜 (extChartAt I' y).toFun (f) (Set.image (extChartAt I x).toFun s)$$
Lean4
/-- One can reformulate smoothness on a set as continuity on this set, and smoothness in any
extended chart in the target. -/
theorem mdifferentiableOn_iff_target :
MDifferentiableOn I I' f s ↔
ContinuousOn f s ∧
∀ y : M', MDifferentiableOn I 𝓘(𝕜, E') (extChartAt I' y ∘ f) (s ∩ f ⁻¹' (extChartAt I' y).source) :=
by
simp only [mdifferentiableOn_iff, ModelWithCorners.source_eq, chartAt_self_eq,
OpenPartialHomeomorph.refl_partialEquiv, PartialEquiv.refl_trans, extChartAt, OpenPartialHomeomorph.extend,
Set.preimage_univ, Set.inter_univ, and_congr_right_iff]
intro h
constructor
· refine fun h' y => ⟨?_, fun x _ => h' x y⟩
have h'' : ContinuousOn _ univ := (ModelWithCorners.continuous I').continuousOn
convert (h''.comp_inter (chartAt H' y).continuousOn_toFun).comp_inter h
simp
· exact fun h' x y => (h' y).2 x 0
