differentiableOn — Mathlib

English

If HasFTaylorSeriesUpToOn n f p s with n≥1, then f is differentiable on s.

Русский

Если существует разложение Тейлора до порядка n≥1, то функция f дифференцируема на s.

LaTeX

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

Lean4

theorem differentiableOn (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) : DifferentiableOn 𝕜 f s := fun _x hx =>
  (h.hasFDerivWithinAt hn hx).differentiableWithinAt

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