mpullback — Mathlib

English

For any f, V, s, x, the pullback within s evaluated at x equals the inverse of the restricted derivative at x applied to V(f(x)).

Русский

Для любых f, V, s, x значение mpullbackWithin на s в точке x равно обратному применению к V(f(x)) производной f, ограниченной на s, в точке x.

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. If the derivative of the map is
not invertible, then pullback is given the junk value zero. -/
def mpullback (f : M → M') (V : Π (x : M'), TangentSpace I' x) (x : M) : TangentSpace I x :=
  (mfderiv I I' f x).inverse (V (f x))

Похожие утверждения