differentiableOn — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem differentiableOn (h : AnalyticOnNhd 𝕜 f s) : DifferentiableOn 𝕜 f s := fun y hy ↦
  (h y hy).differentiableWithinAt

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