fderiv_of_isOpen — Mathlib

English

If f is analytic on an nhd-set s and s is open, then the derivative f' is analytic on s.

Русский

Если функция f аналитична на множестве s в окрестностях и множество s открыто, то ее производная f' аналитична на s.

LaTeX

$$$\text{AnalyticOnNhd } 𝕜 f s \to IsOpen s \to AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s$$$

Lean4

theorem fderiv_of_isOpen (h : AnalyticOnNhd 𝕜 f s) (hs : IsOpen s) : AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s :=
  by
  rw [← hs.analyticOn_iff_analyticOnNhd] at h ⊢
  exact (h.fderivWithin hs.uniqueDiffOn).congr (fun x hx ↦ (fderivWithin_of_isOpen hs hx).symm)

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