English
Let V be differentiable within at t on M' and f be a C^n map on s with invertible mfderiv; the pullback mpullback_vectorField_preimage is C^m on f⁻¹(t).
Русский
Пусть V дифференцируемо внутри t на M' и f — C^n на s, производная mfderiv обратима; тогда mpullback_vectorField_preimage дифференцируемо класса C^m на f⁻¹(t).
LaTeX
$$$\text{If } V \text{ differentiable within at } t, \ f: M\to M' \text{ is } C^n, \ mfderiv \text{ invertible } n\ge2, \text{ then } mpullback\_vectorField\_preimage \in C^m$ on $f^{-1}(t)$. $$
Lean4
theorem _root_.ContMDiffWithinAt.mpullbackWithin_vectorField_inter_of_eq
(hV : ContMDiffWithinAt I' I'.tangent m (fun (y : M') ↦ (V y : TangentBundle I' M')) t y₀)
(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) (h : f x₀ = y₀) :
ContMDiffWithinAt I I.tangent m (fun (y : M) ↦ (mpullbackWithin I I' f V s y : TangentBundle I M)) (s ∩ f ⁻¹' t)
x₀ :=
by
subst h
exact ContMDiffWithinAt.mpullbackWithin_vectorField_inter hV hf hf' hx₀ hs hmn
