English
Let V be a C^m vector field on M and f: M→M' be a C^n map with invertible derivative. Then mpullbackWithin_vectorField' yields a C^m pullback on an appropriate domain.
Русский
Пусть V — векторное поле класса C^m на M, и f: M→M' — отображение класса C^n c обратимой производной; тогда mpullbackWithin_vectorField' даёт пуллбэк класса C^m.
LaTeX
$$$\text{If } V \in C^m, \ f \in C^n, \text{ and } Df \text{ invertible, then } mpullbackWithin\_vectorField' \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, with a set used for the pullback possibly larger. -/
protected theorem _root_.ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq' {u : Set M}
(hV : ContMDiffWithinAt I' I'.tangent m (fun (y : M') ↦ (V y : TangentBundle I' M')) t y₀)
(hf : ContMDiffWithinAt I I' n f u x₀) (hf' : (mfderivWithin I I' f u x₀).IsInvertible) (hx₀ : x₀ ∈ s)
(hs : UniqueMDiffOn I s) (hmn : m + 1 ≤ n) (hst : f ⁻¹' t ∈ 𝓝[s] x₀) (hu : s ⊆ u) (hy₀ : f x₀ = y₀) :
ContMDiffWithinAt I I.tangent m (fun (y : M) ↦ (mpullbackWithin I I' f V u y : TangentBundle I M)) s x₀ :=
by
subst hy₀
exact ContMDiffWithinAt.mpullbackWithin_vectorField' hV hf hf' hx₀ hs hmn hst hu
