English
If V is C^m along M' within t and f is C^n with y0=f(x0) and invertible derivative, then mpullbackWithin_vectorField_of_mem_of_eq gives a C^m pullback on s.
Русский
Если V — C^m вдоль M' внутри t, и f — C^n с равенством y0=f(x0) и обратимой производной, то mpullbackWithin_vectorField_of_mem_of_eq даёт пуллбэк класса C^m на s.
LaTeX
$$$\text{Under } y_0=f(x_0) \text{ and invertible mfderivWithin } mpullbackWithin_vectorField_of_mem_of_eq \text{ is } 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 on a set. -/
protected theorem _root_.ContMDiffOn.mpullbackWithin_vectorField_inter
(hV : ContMDiffOn I' I'.tangent m (fun (y : M') ↦ (V y : TangentBundle I' M')) t) (hf : ContMDiffOn I I' n f s)
(hf' : ∀ x ∈ s ∩ f ⁻¹' t, (mfderivWithin I I' f s x).IsInvertible) (hs : UniqueMDiffOn I s) (hmn : m + 1 ≤ n) :
ContMDiffOn I I.tangent m (fun (y : M) ↦ (mpullbackWithin I I' f V s y : TangentBundle I M)) (s ∩ f ⁻¹' t) :=
fun _ hx₀ ↦ ContMDiffWithinAt.mpullbackWithin_vectorField_inter (hV _ hx₀.2) (hf _ hx₀.1) (hf' _ hx₀) hx₀.1 hs hmn
