English
Under the standard hypotheses for m+1 ≤ n, the pullback mpullbackWithin_vectorField_inter is ContMDiffWithinAt of order m along the pulled back field on the intersection domain.
Русский
При стандартных предпосылках m+1 ≤ n пуллбэк mpullbackWithin_vectorField_inter является ContMDiffWithinAt порядка m вдоль вытянутого поля на пересечении доменов.
LaTeX
$$$\text{Under } m+1 \le n, \ mpullbackWithin( V, f, s, t ) \in ContMDiffWithinAt.$$$
Lean4
/-- The pullback of a differentiable vector field by a `C^n` function with `2 ≤ n` is
differentiable. -/
protected theorem _root_.MDifferentiable.mpullback_vectorField
(hV : MDifferentiable I' I'.tangent (fun (y : M') ↦ (V y : TangentBundle I' M'))) (hf : ContMDiff I I' n f)
(hf' : ∀ x, (mfderiv I I' f x).IsInvertible) (hmn : 2 ≤ n) :
MDifferentiable I I.tangent (fun (y : M) ↦ (mpullback I I' f V y : TangentBundle I M)) := fun x ↦
MDifferentiableAt.mpullback_vectorField (hV (f x)) (hf x) (hf' x) hmn
