English
The Taylor series up to n+1 is equivalent to the Taylor series up to n, together with the derivative of the n-th term and the continuity of the (n+1)-st term.
Русский
Разложение Тейлора до n+1 эквивалентно разложению до n плюс производная n-й термы и непрерывность (n+1)-й термы.
LaTeX
$$$$\text{HasFTaylorSeriesUpToOn}(n+1,f,p,s) \iff \Big(\text{HasFTaylorSeriesUpToOn}(n,f,p,s)\Big) \wedge \Big(\forall x\in s, \text{HasFDerivWithinAt}(f, p x n, s, x)\Big) \wedge \Big(\text{ContinuousOn}(p\,\cdot\,(n+1), s)\Big).$$$$
Lean4
/-- If a function has a Taylor series at order at least `1` on a neighborhood of `x`, then the term
of order `1` of this series is a derivative of `f` at `x`. -/
theorem hasFDerivAt (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) (hx : s ∈ 𝓝 x) :
HasFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p x 1)) x :=
(h.hasFDerivWithinAt hn (mem_of_mem_nhds hx)).hasFDerivAt hx
