English
The MF-derivative within a set s, mfderivWithin, is defined to be the coordinate derivative if differentiable within, and zero otherwise; this yields a continuous linear map from T_x M to T_{f(x)} M'.
Русский
MF-производная внутри множества s — это координатная производная, если существует внутри, и в противном случае ноль; получается непрерывное линейное отображение между касательными пространствами.
LaTeX
$$$\mathrm{mfderivWithin}(f,s,x) = \begin{cases} f'_{coord} & \text{если } MDifferentiableWithinAt(I,I')(f,s,x), \\ 0 & \text{иначе}, \end{cases}$$$
Lean4
/-- Let `f` be a function between two manifolds. Then `mfderivWithin I I' f s x` is the
derivative of `f` at `x` within `s`, as a continuous linear map from the tangent space at `x` to the
tangent space at `f x`. -/
def mfderivWithin (f : M → M') (s : Set M) (x : M) : TangentSpace I x →L[𝕜] TangentSpace I' (f x) :=
if MDifferentiableWithinAt I I' f s x then
(fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((extChartAt I x).symm ⁻¹' s ∩ range I) ((extChartAt I x) x) : _)
else 0
