English
If y0 = f(x0), then the contMDiff mpullback_vectorField_preimage_of_eq holds, giving C^m differentiability for the pullback at x0.
Русский
Если y0 = f(x0), то ContMDiff mpullback_vectorField_preimage_of_eq обеспечивает C^m-дифференцируемость пуллбэк в точке x0.
LaTeX
$$$\text{If } y_0=f(x_0), \text{ then } ContMDiffWithinAt(mpullback_vectorField_preimage\_eq) \text{ holds.}$$$
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_of_mem_nhdsWithin
(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)
(hst : f ⁻¹' t ∈ 𝓝[s] x₀) :
ContMDiffWithinAt I I.tangent m (fun (y : M) ↦ (mpullback I I' f V y : TangentBundle I M)) s x₀ :=
(ContMDiffWithinAt.mpullback_vectorField_preimage hV hf hf' hmn).mono_of_mem_nhdsWithin hst
