English
The pullback within a set of a vector field V under a map f is given by (DfWithin f s x)^{-1}(V(f(x))), with the convention that if the derivative is not invertible a default junk value is used.
Русский
Тяга обратно внутри множества векторного поля V по отображению f задаётся формулой (DfWithin f s x)^{-1}(V(f(x))), если производная обратима; иначе используется произвольное значение.
LaTeX
$$$ pullbackWithin 𝕜 f V s x = (fderivWithin 𝕜 f s x)^{-1} (V (f x)) $$$
Lean4
/-- The pullback within a set of a vector field under a function, defined
as `(f^* V) (x) = Df(x)^{-1} (V (f x))` where `Df(x)` is the derivative of `f` within `s`.
If `Df(x)` is not invertible, we use the junk value `0`.
-/
def pullbackWithin (f : E → F) (V : F → F) (s : Set E) (x : E) : E :=
(fderivWithin 𝕜 f s x).inverse (V (f x))
