English
If a function f has a formal power series p representing it within a subset s around a point x, and x is a unique differentiability point for the union of {x} and s, then the derivative inside the enlarged domain is given by the first coefficient of p, transported by the natural currying to the target space.
Русский
Если функция f имеет формальную степенную серию p, представляющую её внутри области s в окрестности точки x, и точка x является уникально дифференцируемой для объединения {x} с s, то производная внутри расширенной области равна первой коэффиценте p, приведённой к целевому пространству через естественную каррировку.
LaTeX
$$$f\\text{ derWithin}_{\\mathbb{K}} f (\\text{insert } x\, s)\, x = \\operatorname{continuousMultilinearCurryFin1}_{\\mathbb{K}} E F (p\,1)$$$
Lean4
theorem fderivWithin_eq (h : HasFPowerSeriesWithinAt f p s x) (hu : UniqueDiffWithinAt 𝕜 (insert x s) x) :
fderivWithin 𝕜 f (insert x s) x = continuousMultilinearCurryFin1 𝕜 E F (p 1) :=
h.hasFDerivWithinAt.fderivWithin hu
