English
If y0 = f(x0), the pullback mpullback_vectorField_preimage respects the equality and yields differentiability of the pulled vector field at x0 with the same hypotheses as the general mpullback.
Русский
Если y0 = f(x0), пуллбэк mpullback_vectorField_preimage сохраняет равенство и даёт дифференцируемость вытянутого векторного поля в точке x0 при тех же предпосылках, что и общий пуллбэк.
LaTeX
$$$\text{If } y_0 = f(x_0), \ V, f, \text{ and invertibility hold, then } mpullback\_vectorField\_preimage \text{ is } C^m \, at \, x_0.$$$
Lean4
/-- The pullback of a differentiable vector field by a `C^n` function with `2 ≤ n` is
differentiable. Version within a set at a point, but with full pullback. -/
protected theorem _root_.MDifferentiableWithinAt.mpullback_vectorField_preimage_of_eq
(hV : MDifferentiableWithinAt I' I'.tangent (fun (y : M') ↦ (V y : TangentBundle I' M')) t y₀)
(hf : ContMDiffAt I I' n f x₀) (hf' : (mfderiv I I' f x₀).IsInvertible) (hmn : 2 ≤ n) (hy₀ : y₀ = f x₀) :
MDifferentiableWithinAt I I.tangent (fun (y : M) ↦ (mpullback I I' f V y : TangentBundle I M)) (f ⁻¹' t) x₀ :=
by
subst hy₀
exact hV.mpullback_vectorField_preimage hf hf' hmn
