English
Let f: M → M′ be a map between manifolds, and let V be a vector field on M′ defined on a subset s ⊆ M. The pullback of V under f inside s is the tangent vector at x ∈ s given by the inverse of the derivative of f (restricted to s) applied to V at f(x). If the restricted derivative is not invertible, the pullback is defined to be the junk value zero. Symbolically, mpullbackWithin I I′ f V s x = (mfderivWithin I I′ f s x)^{-1}(V(f(x))).
Русский
Если два векторных поля — ContMDiffWithinAt на s, их скобка также ContMDiffWithinAt на s.
LaTeX
$$$\mathrm{mpullbackWithin}\ I\ I'\ f\ V\ s\ x = \left(\mathrm{mfderivWithin}\ I\ I'\ f\ s\ x\right)^{-1}\bigl(V(f(x))\bigr)$$$
Lean4
/-- The pullback of a vector field under a map between manifolds, within a set `s`. If the
derivative of the map within `s` is not invertible, then pullback is given the junk value zero. -/
def mpullbackWithin (f : M → M') (V : Π (x : M'), TangentSpace I' x) (s : Set M) (x : M) : TangentSpace I x :=
(mfderivWithin I I' f s x).inverse (V (f x))
