English
The derivative within a set acts as a map between tangent bundles: it sends a point p = (x,v) with x ∈ M to (f(x), df_x(v)) in TangentBundle I' M'.
Русский
Производная внутри множества реализуется как отображение между касательными пучками: p=(x,v) → (f(x), df_x(v)).
LaTeX
$$$\\mathrm{tangentMapWithin}(f,s) : \\mathrm{TangentBundle}(I,M) \\to \\mathrm{TangentBundle}(I',M') \;\\text{defined by } p \\mapsto \\bigl(f(p.1), \\mathrm{mfderivWithin}(I,I',f,s)(p.1)(p.2)\\bigr).$$$
Lean4
/-- Let `f` be a function between two manifolds. Then `mfderiv I I' f x` is the derivative of
`f` at `x`, as a continuous linear map from the tangent space at `x` to the tangent space at
`f x`. -/
def mfderiv (f : M → M') (x : M) : TangentSpace I x →L[𝕜] TangentSpace I' (f x) :=
if MDifferentiableAt I I' f x then
(fderivWithin 𝕜 (writtenInExtChartAt I I' x f : E → E') (range I) ((extChartAt I x) x) :)
else 0
