English
If y0 = f(x0), then mpullback_vectorField_preimage_of_eq holds, giving C^m differentiability of the pullback at x0 under the standard hypotheses.
Русский
Если y0 = f(x0), то mpullback_vectorField_preimage_of_eq обеспечивает дифференцируемость пуллбэк-векторного поля в точке x0 при стандартных предпосылках.
LaTeX
$$$\text{If } y_0 = f(x_0), \text{then } ContMDiffWithinAt(mpullback\_vectorField\_preimage\_of\_eq) \text{ holds with } C^m. $$$
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. -/
protected theorem _root_.ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem
(hV : ContMDiffWithinAt I' I'.tangent m (fun (y : M') ↦ (V y : TangentBundle I' M')) t (f x₀))
(hf : ContMDiffWithinAt I I' n f s x₀) (hf' : (mfderivWithin I I' f s x₀).IsInvertible) (hx₀ : x₀ ∈ s)
(hs : UniqueMDiffOn I s) (hmn : m + 1 ≤ n) (hst : f ⁻¹' t ∈ 𝓝[s] x₀) :
ContMDiffWithinAt I I.tangent m (fun (y : M) ↦ (mpullbackWithin I I' f V s y : TangentBundle I M)) s x₀ :=
by
apply (ContMDiffWithinAt.mpullbackWithin_vectorField_inter hV hf hf' hx₀ hs hmn).mono_of_mem_nhdsWithin
exact Filter.inter_mem self_mem_nhdsWithin hst
