deriv — Mathlib

English

If a function is analytic on a nhd set, then its derivative is analytic on that nhd set.

Русский

Если функция аналитична на окрестности множества nhd, то ее производная аналитична на этом nhd.

LaTeX

$$protected theorem deriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) : AnalyticOnNhd 𝕜 (deriv f) s$$

Lean4

/-- If a function is analytic on a set `s` in a complete space, so is its derivative. -/
protected theorem deriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) : AnalyticOnNhd 𝕜 (deriv f) s :=
  (ContinuousLinearMap.apply 𝕜 F (1 : 𝕜)).comp_analyticOnNhd h.fderiv

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