English
A more explicit symmetric version of the pullback differentiability result in the extChartAt_symm setting, yielding C^m on the appropriate domain.
Русский
Более явная симметричная версия результата дифференцируемости пуллбэк в настройке extChartAt_symm, дающая C^m на нужном домене.
LaTeX
$$$\text{Under } extChartAt\_symm, \ mpullbackWithin \text{ is } C^m.$$
Lean4
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.
Version at a point. -/
protected theorem _root_.ContMDiffAt.mpullback_vectorField_preimage
(hV : ContMDiffAt I' I'.tangent m (fun (y : M') ↦ (V y : TangentBundle I' M')) (f x₀))
(hf : ContMDiffAt I I' n f x₀) (hf' : (mfderiv I I' f x₀).IsInvertible) (hmn : m + 1 ≤ n) :
ContMDiffAt I I.tangent m (fun (y : M) ↦ (mpullback I I' f V y : TangentBundle I M)) x₀ :=
by
simp only [← contMDiffWithinAt_univ] at hV hf hf' ⊢
simpa using ContMDiffWithinAt.mpullback_vectorField_preimage hV hf hf' hmn
