English
If e and e' come from maximal atlases around x and f x, and s is contained in the source of e with maps into the source of e', then MDifferentiableOn f on s is equivalent to differentiability on the extended charts on the image.
Русский
Если карты e и e' из максимальных атласов вокруг x и f(x), и s ⊆ source e сображением в source e', то MDifferentiableOn равносильно дифференцируемости в расширенных картах на образе s.
LaTeX
$$MDifferentiableOn I I' f s ↔ ContinuousOn f s ∧ DifferentiableOn 𝕜 (e'.extend I' ∘ f ∘ (e.extend I).symm) (e.extend I '' s)$$
Lean4
/-- One can reformulate smoothness on a set as continuity on this set, and smoothness in any
extended chart. -/
theorem mdifferentiableOn_iff :
MDifferentiableOn I I' f s ↔
ContinuousOn f s ∧
∀ (x : M) (y : M'),
DifferentiableOn 𝕜 (extChartAt I' y ∘ f ∘ (extChartAt I x).symm)
((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) :=
by
constructor
· intro h
refine ⟨fun x hx => (h x hx).1, fun x y z hz => ?_⟩
simp only [mfld_simps] at hz
let w := (extChartAt I x).symm z
have : w ∈ s := by simp only [w, hz, mfld_simps]
specialize h w this
have w1 : w ∈ (chartAt H x).source := by simp only [w, hz, mfld_simps]
have w2 : f w ∈ (chartAt H' y).source := by simp only [w, hz, mfld_simps]
convert ((mdifferentiableWithinAt_iff_of_mem_source w1 w2).mp h).2.mono _
· simp only [w, hz, mfld_simps]
· mfld_set_tac
· rintro ⟨hcont, hdiff⟩ x hx
refine differentiableWithinAt_localInvariantProp.liftPropWithinAt_iff.mpr ?_
refine ⟨hcont x hx, ?_⟩
dsimp [DifferentiableWithinAtProp]
convert hdiff x (f x) (extChartAt I x x) (by simp only [hx, mfld_simps]) using 1
mfld_set_tac
