differentiable — Mathlib

English

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

Русский

Если на множестве s выполнено HasFTaylorSeriesUpToOn n f p s и n ≥ 1, то функция f дифференцируема на s.

LaTeX

$$$\text{HasFTaylorSeriesUpToOn } n f p s \land 1 \le n \implies \text{Differentiable } 𝕜 f$$$

Lean4

theorem differentiable (h : HasFTaylorSeriesUpTo n f p) (hn : 1 ≤ n) : Differentiable 𝕜 f := fun x =>
  (h.hasFDerivAt hn x).differentiableAt

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