differentiableAt — Mathlib

English

If h has a Taylor series up to n with n≥1, then for each x∈s, HasFDerivWithinAt holds with the first derivative term p x 1, and the curry-left of that term.

Русский

Если у h разложение до n≥1, то для каждого x∈s выполняется HasFDerivWithinAt с первой производной p x 1 и соответствующим curryLeft.

LaTeX

$$$$\text{HasFTaylorSeriesUpToOn}(n,f,p,s) \land 1 \le n \Rightarrow \text{HasFDerivWithinAt}(f, \text{continuousMultilinearCurryFin1}(p\,x\,1), s, x).$$$$

Lean4

/-- If a function has a Taylor series at order at least `1` on a neighborhood of `x`, then
it is differentiable at `x`. -/
theorem differentiableAt (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) (hx : s ∈ 𝓝 x) : DifferentiableAt 𝕜 f x :=
  (h.hasFDerivAt hn hx).differentiableAt

Похожие утверждения