English
Let V be differentiable within At I' I'.tangent on t and f : M → M' be a C^n map on s with invertible derivative everywhere. Then the pullback vector field mpullback I I' f V is differentiable on f⁻¹(t).
Русский
Пусть V дифференцируемо внутри множества на t, а f: M→M' — C^n с обратимой производной; тогда пуллбэк векторного поля mpullback на f⁻¹(t) дифференцируем.
LaTeX
$$$\text{If } V: M' \to TM' \text{ is differentiable within } t, \ f: M \to M' \text{ is } C^n, \ mfderiv(I,I',f) \text{ invertible, then } mpullback(I,I',f,V) \text{ is differentiable on } f^{-1}(t).$$$
Lean4
/-- The pullback of a differentiable vector field by a `C^n` function with `2 ≤ n` is
differentiable. Version within a set at a point, but with full pullback. -/
protected theorem _root_.MDifferentiableWithinAt.mpullback_vectorField_preimage
(hV : MDifferentiableWithinAt I' I'.tangent (fun (y : M') ↦ (V y : TangentBundle I' M')) t (f x₀))
(hf : ContMDiffAt I I' n f x₀) (hf' : (mfderiv I I' f x₀).IsInvertible) (hmn : 2 ≤ n) :
MDifferentiableWithinAt I I.tangent (fun (y : M) ↦ (mpullback I I' f V y : TangentBundle I M)) (f ⁻¹' t) x₀ :=
by
simp only [← contMDiffWithinAt_univ, ← mfderivWithin_univ, ← mpullbackWithin_univ] at hV hf hf' ⊢
simpa using hV.mpullbackWithin_vectorField_inter hf hf' (mem_univ _) uniqueMDiffOn_univ hmn
