English
If y0 = f(x0) and the derivatives are invertible, the mpullback vector field pulled back by f at x0 is C^m on the preimage domain.
Русский
Если y0 = f(x0) и производные обратимы, пуллбэк-векторное поле, вытянутое по f в точке x0, является C^m на области предобраза.
LaTeX
$$$\text{If } y_0=f(x_0), \ mpullback\_vectorField\_preimage \text{ is } C^m \text{ at } x_0.$$$
Lean4
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.
Version within a set at a point, but with full pullback. -/
protected theorem _root_.ContMDiffWithinAt.mpullback_vectorField_preimage
(hV : ContMDiffWithinAt I' I'.tangent m (fun (y : M') ↦ (V y : TangentBundle I' M')) t (f x₀))
(hf : ContMDiffAt I I' n f x₀) (hf' : (mfderiv I I' f x₀).IsInvertible) (hmn : m + 1 ≤ n) :
ContMDiffWithinAt I I.tangent m (fun (y : M) ↦ (mpullback I I' f V y : TangentBundle I M)) (f ⁻¹' t) x₀ :=
by
simp only [← contMDiffWithinAt_univ, ← mfderivWithin_univ, ← mpullbackWithin_univ] at hV hf hf' ⊢
simpa using hV.mpullbackWithin_vectorField_inter hf hf' (mem_univ _) uniqueMDiffOn_univ hmn
