English
Let V be a C^m vector field along M' and f be a C^n map with m+1 ≤ n; then mpullbackWithin_vectorField_inter shows mpullbackWithin yields a C^m vector field on the suitable domain.
Русский
Пусть V — векторное поле класса C^m вдоль M', и f — отображение класса C^n с m+1 ≤ n; тогда mpullbackWithin_vectorField_inter доказывает, что пуллбэк вместе с областью определения даёт векторное поле класса C^m на соответствующей области.
LaTeX
$$$\text{If } V \in C^m, \ f \in C^n, \ m+1 \le n, \text{ then } mpullbackWithin(V,f) \in C^m.$$$
Lean4
/-- The pullback of a differentiable vector field by a `C^n` function with `2 ≤ n` is
differentiable. Version at a point. -/
protected theorem _root_.MDifferentiableAt.mpullback_vectorField
(hV : MDifferentiableAt I' I'.tangent (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 : 2 ≤ n) :
MDifferentiableAt I I.tangent (fun (y : M) ↦ (mpullback I I' f V y : TangentBundle I M)) x₀ := by
simpa using MDifferentiableWithinAt.mpullback_vectorField_preimage hV hf hf' hmn
