English
If V is C^m on M' and f: M→M' is C^n with invertible mfderiv, then mpullback_vectorField is C^m on M.
Русский
Если V — C^m на M', и f: M→M' — C^n с обратимой mfderiv, то mpullback_vectorField — C^m на M.
LaTeX
$$$\text{If } V \in C^m, \ f \in C^n, \ mfderiv(f) \text{ invertible, then } mpullback(V,f) \in 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, but with full pullback. -/
protected theorem _root_.ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin_of_eq
(hV : ContMDiffWithinAt I' I'.tangent m (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 : m + 1 ≤ n) (hst : f ⁻¹' t ∈ 𝓝[s] x₀)
(hy₀ : y₀ = f x₀) :
ContMDiffWithinAt I I.tangent m (fun (y : M) ↦ (mpullback I I' f V y : TangentBundle I M)) s x₀ :=
by
subst hy₀
exact ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin hV hf hf' hmn hst
