deriv — Mathlib

English

If f is analytic at x, then for every n, the nth iterated derivative is analytic at x.

Русский

Если f аналитична в точке x, то для каждого n-ого производная является аналитичной в x.

LaTeX

$$$\text{AnalyticAt 𝕜 } f x \to \forall n : \mathbb{N}, AnalyticAt 𝕜 (\mathrm{deriv}^{(n)} f) x$$$

Lean4

protected theorem deriv [CompleteSpace F] (h : AnalyticAt 𝕜 f x) : AnalyticAt 𝕜 (deriv f) x :=
  by
  obtain ⟨r, hr, h⟩ := h.exists_ball_analyticOnNhd
  exact h.deriv x (by simp [hr])

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