English
If y0 = f(x0), equality is preserved through the pullback preimage construction, yielding a differentiable pullback at x0 of class C^m.
Русский
Если y0 = f(x0), равенство сохраняется через конструирование preimage пуллбэк, и получается дифференцируемое пуллбэк-поле класса C^m в точке x0.
LaTeX
$$$\text{If } y_0=f(x_0), \ mpullback_vectorField_preimage_of_eq \text{ gives } C^m \text{ pullback 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`. -/
protected theorem _root_.ContMDiff.mpullback_vectorField
(hV : ContMDiff I' I'.tangent m (fun (y : M') ↦ (V y : TangentBundle I' M'))) (hf : ContMDiff I I' n f)
(hf' : ∀ x, (mfderiv I I' f x).IsInvertible) (hmn : m + 1 ≤ n) :
ContMDiff I I.tangent m (fun (y : M) ↦ (mpullback I I' f V y : TangentBundle I M)) := fun x ↦
ContMDiffAt.mpullback_vectorField_preimage (hV (f x)) (hf x) (hf' x) hmn
