iteratedFDeriv_of_isOpen — Mathlib

English

If f is analytic on an open nhd-set s, then for every natural number n, the nth iterated derivative of f is analytic on s.

Русский

Если f аналитична на открытом множестве s, то для любого натурального числа n n-ая итерационная производная f аналитична на s.

LaTeX

$$$\text{AnalyticOnNhd } 𝕜 f s \to IsOpen s \to \forall n : \mathbb{N}, AnalyticOnNhd 𝕜 (\text{iteratedFDeriv } 𝕜 n f) s$$$

Lean4

theorem iteratedFDeriv_of_isOpen (h : AnalyticOnNhd 𝕜 f s) (hs : IsOpen s) (n : ℕ) :
    AnalyticOnNhd 𝕜 (iteratedFDeriv 𝕜 n f) s :=
  by
  rw [← hs.analyticOn_iff_analyticOnNhd] at h ⊢
  exact (h.iteratedFDerivWithin hs.uniqueDiffOn n).congr (fun x hx ↦ (iteratedFDerivWithin_of_isOpen n hs hx).symm)

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