English
At a point x, the MF-differential f' exists as a continuous linear map from T_x M to T_{f(x)} M' when f is differentiable at x in the manifold sense.
Русский
В точке x существует MF-производная f' как непрерывно линейное отображение от касательного пространства T_x M к T_{f(x)} M', если f дифференцируема в точке x на многообразии.
LaTeX
$$$\mathrm{HasMFDerivAt}(f,x,f') \iff \mathrm{ContinuousAt}(f,x) \land \mathrm{HasFDerivWithinAt}(\mathrm{writtenInExtChartAt}(I,I',x,f) : E\to E')\; f'\; (\mathrm{range}(I))\; ((\mathrm{extChartAt}(I,x) x)).$$$
Lean4
/-- `HasMFDerivAt I I' f x f'` indicates that the function `f` between manifolds
has, at the point `x`, the derivative `f'`. Here, `f'` is a continuous linear
map from the tangent space at `x` to the tangent space at `f x`.
We require continuity in the definition, as otherwise points close to `x` in `s` could be sent by
`f` outside of the chart domain around `f x`. Then the chart could do anything to the image points,
and in particular by coincidence `writtenInExtChartAt I I' x f` could be differentiable, while
this would not mean anything relevant. -/
def HasMFDerivAt (f : M → M') (x : M) (f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)) :=
ContinuousAt f x ∧ HasFDerivWithinAt (writtenInExtChartAt I I' x f : E → E') f' (range I) ((extChartAt I x) x)
