English
If f is differentiable within at, then its written-in-ext-chart-at form is differentiable within at on the appropriate domain.
Русский
Если f дифференцируема внутри множества, то её запись в расширенной карте диаграммы дифференцируема на соответствующей области.
LaTeX
$$$\text{MDifferentiableWithinAt.differentiableWithinAt_writtenInExtChartAt } f s x :\ \text{DifferentiableWithinAt } 𝕜 (writtenInExtChartAt I I' x f) (\text{range } I) ((\text{extChartAt } I x) x)$$$
Lean4
/-- `MDifferentiableWithinAt I I' f s x` indicates that the function `f` between manifolds
has a derivative at the point `x` within the set `s`.
This is a generalization of `DifferentiableWithinAt` to manifolds.
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 MDifferentiableWithinAt (f : M → M') (s : Set M) (x : M) :=
LiftPropWithinAt (DifferentiableWithinAtProp I I') f s x
