English
At a point x of a manifold map f, the MF-derivative within a set s exists as a linear map f' between tangent spaces, provided f is continuous in s at x and the coordinate derivative exists inside a chart.
Русский
В точке x отображения f на многообразии производная MF внутри множества s существует как линейное отображение между касательными пространствами, если f непрерывна в s в точке x и существует координатная производная в чарте.
LaTeX
$$$\mathrm{HasMFDerivWithinAt}(f,s,x,f') \iff \mathrm{ContinuousWithinAt}(f,s,x) \land \mathrm{HasFDerivWithinAt}(\mathrm{writtenInExtChartAt}(I,I',x,f) : E\to E')\; f'\; ((\mathrm{extChartAt}(I,x)^{-1} s)\cap \mathrm{range}(I))\; ((\mathrm{extChartAt}(I,x))x).$$$
Lean4
/-- `HasMFDerivWithinAt I I' f s x f'` indicates that the function `f` between manifolds
has, at the point `x` and within the set `s`, the derivative `f'`. Here, `f'` is a continuous linear
map from the tangent space at `x` to the tangent space at `f x`.
This is a generalization of `HasFDerivWithinAt` to manifolds (as indicated by the prefix `m`).
The order of arguments is changed as the type of the derivative `f'` depends on the choice of `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 HasMFDerivWithinAt (f : M → M') (s : Set M) (x : M) (f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)) :=
ContinuousWithinAt f s x ∧
HasFDerivWithinAt (writtenInExtChartAt I I' x f : E → E') f' ((extChartAt I x).symm ⁻¹' s ∩ range I)
((extChartAt I x) x)
