fderiv — Mathlib

English

If a function is analytic on a neighborhood, then it is differentiable on that neighborhood.

Русский

Если функция аналитична на окрестности, то она дифференцируема на этой окрестности.

LaTeX

$$$\\text{AnalyticOnNhd } f s \\Rightarrow \\text{DifferentiableOn } f s$$$

Lean4

/-- If a function is analytic on a set `s`, so is its Fréchet derivative. See also
`AnalyticOnNhd.fderiv_of_isOpen`, removing the completeness assumption but requiring the set
to be open. -/
protected theorem fderiv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) : AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s := fun y hy ↦
  AnalyticAt.fderiv (h y hy)

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