English
If V is differentiable along t on M' and f x0 = y0, with the usual hypotheses for the m + 1 ≤ n case, then the pullback mpullbackWithin V s y corresponds at x0 to the pullback mpullbackWithin evaluated at the preimage domain where y0 = f(x0).
Русский
Если V дифференцируемо на t на M' и f(x0) = y0, при всех обычных предпосылках для случая m + 1 ≤ n, то пуллбэк mpullbackWithin V имеет соответствие в точке x0 через домен предобраза, где y0 = f(x0).
LaTeX
$$$\text{If } V: M' \to TM' \text{ is } C^m, \ f: M \to M' \text{ is } C^n, \ y_0 = f(x_0), \text{ and hypotheses hold, then } \\ mpullbackWithin(I,I',f,V, s,t)\big|_{x_0} ext{ is } C^m.$$$
Lean4
/-- The pullback of a differentiable vector field by a `C^n` function with `2 ≤ n` is
differentiable. Version on a set. -/
protected theorem _root_.MDifferentiableOn.mpullbackWithin_vectorField_inter
(hV : MDifferentiableOn I' I'.tangent (fun (y : M') ↦ (V y : TangentBundle I' M')) t) (hf : ContMDiffOn I I' n f s)
(hf' : ∀ x ∈ s ∩ f ⁻¹' t, (mfderivWithin I I' f s x).IsInvertible) (hs : UniqueMDiffOn I s) (hmn : 2 ≤ n) :
MDifferentiableOn I I.tangent (fun (y : M) ↦ (mpullbackWithin I I' f V s y : TangentBundle I M)) (s ∩ f ⁻¹' t) :=
fun _ hx₀ ↦
MDifferentiableWithinAt.mpullbackWithin_vectorField_inter (hV _ hx₀.2) (hf _ hx₀.1) (hf' _ hx₀) hx₀.1 hs hmn
