deriv — Mathlib

English

If f is analytic on nhd, then its derivative is analytic on nhd.

Русский

Если f аналитична на окрестности nhd, то её производная аналитична на nhd.

LaTeX

$$$\text{AnalyticOnNhd } 𝕜 f s \Rightarrow \text{AnalyticOnNhd } 𝕜 (\deriv f) s$$$

Lean4

/-- If a function is polynomial on a set `s`, so is its derivative. -/
protected theorem deriv (h : CPolynomialOn 𝕜 f s) : CPolynomialOn 𝕜 (deriv f) s :=
  (ContinuousLinearMap.apply 𝕜 F (1 : 𝕜)).comp_cpolynomialOn h.fderiv

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