English
If h₁V and h₂ are equal in the relevant coordinates, the pullback mpullbackWithin_vectorField_inter_of_eq holds, giving differentiability of the pulled vector field on the intersection domain with y0 = f(x0).
Русский
Если канонические представления V совпадают в нужной координатной системе, то равенство удерживает дифференцируемость пула mpullbackWithin_vectorField_inter_of_eq на пересечении доменов.
LaTeX
$$$\text{If } hV, hf, hf', hx_0, hs, hmn, h : y_0 = f(x_0) \text{ then } MDifferentiableWithinAt I I.tangent(\cdot) \text{ on } s \cap f^{-1}(t).$$$
Lean4
/-- The pullback of a differentiable vector field by a `C^n` function with `2 ≤ n` is
differentiable. Version on a set, but with full pullback -/
protected theorem _root_.MDifferentiableOn.mpullback_vectorField_preimage
(hV : MDifferentiableOn I' I'.tangent (fun (y : M') ↦ (V y : TangentBundle I' M')) t) (hf : ContMDiff I I' n f)
(hf' : ∀ x ∈ f ⁻¹' t, (mfderiv I I' f x).IsInvertible) (hmn : 2 ≤ n) :
MDifferentiableOn I I.tangent (fun (y : M) ↦ (mpullback I I' f V y : TangentBundle I M)) (f ⁻¹' t) := fun x₀ hx₀ ↦
MDifferentiableWithinAt.mpullback_vectorField_preimage (hV _ hx₀) (hf x₀) (hf' _ hx₀) hmn
