English
The tangent map assigns to each point p = (x,v) the pair (f(x), df_x(v)), giving a linear approximation of f on tangent vectors.
Русский
Касательное отображение сопоставляет каждому п = (x, v) пару (f(x), df_x(v)), задавая линейную аппроксимацию f на касательных векторх.
LaTeX
$$$\mathrm{tangentMap}(f) : \mathrm{TangentBundle}(I,M) \to \mathrm{TangentBundle}(I',M'),\quad \mathrm{tangentMap}(f)(p) = \bigl(f(p.1), (\mathrm{mfderiv}(I,I',f))(p.1)(p.2)\bigr).$$$
Lean4
/-- The derivative within a set, as a map between the tangent bundles -/
def tangentMapWithin (f : M → M') (s : Set M) : TangentBundle I M → TangentBundle I' M' := fun p =>
⟨f p.1, (mfderivWithin I I' f s p.1 : TangentSpace I p.1 → TangentSpace I' (f p.1)) p.2⟩
