deriv_of_isOpen — Mathlib

English

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

Русский

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

LaTeX

$$$\text{deriv_of_isOpen } (h) (hs) : AnalyticOnNhd 𝕜 (deriv f) s$$$

Lean4

/-- If a function is analytic on an open set `s`, so is its derivative. -/
theorem deriv_of_isOpen (h : AnalyticOnNhd 𝕜 f s) (hs : IsOpen s) : AnalyticOnNhd 𝕜 (deriv f) s :=
  (ContinuousLinearMap.apply 𝕜 F (1 : 𝕜)).comp_analyticOnNhd (h.fderiv_of_isOpen hs)

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