English
Let V be a C^m vector field on M' and f: M → M' be a C^n map with n ≥ 2. If V is differentiable along t in M', and f is C^n on s, with mfderivWithin invertible, then the pullback mpullbackWithin of V along f is C^m on s ∩ f⁻¹(t).
Русский
Пусть V — векторное поле класса C^m на M', и f: M → M' — отображение класса C^n, n ≥ 2. Если V дифференцируемо на t в M', и f — C^n на s, причём mfderivWithin обратима, то пуллбэк mpullbackWithin V along f имеет класс C^m на s ∩ f⁻¹(t).
LaTeX
$$$\text{Let } V: M' \to TM' \text{ be } C^m, \; f: M \to M' \text{ be } C^n,\; n \ge 2. \\ \\ V \text{ is differentiable along } t, \; hf: f \text{ is } C^n \text{ on } s, \; (mfderivWithin I I' f s x) \text{ invertible. Then } \\ (x \mapsto mpullbackWithin I I' f V s x) \text{ is } C^m \text{ on } s. }$$$
Lean4
theorem _root_.MDifferentiableWithinAt.mpullbackWithin_vectorField_inter_of_eq
(hV : MDifferentiableWithinAt I' I'.tangent (fun (y : M') ↦ (V y : TangentBundle I' M')) t y₀)
(hf : ContMDiffWithinAt I I' n f s x₀) (hf' : (mfderivWithin I I' f s x₀).IsInvertible) (hx₀ : x₀ ∈ s)
(hs : UniqueMDiffOn I s) (hmn : 2 ≤ n) (h : y₀ = f x₀) :
MDifferentiableWithinAt I I.tangent (fun (y : M) ↦ (mpullbackWithin I I' f V s y : TangentBundle I M)) (s ∩ f ⁻¹' t)
x₀ :=
by
subst h
exact hV.mpullbackWithin_vectorField_inter hf hf' hx₀ hs hmn
