analyticOnNhd — Mathlib

English

For an open set, analytic on the set is equivalent to differentiable on the set.

Русский

Для открытого множества аналитичность эквивалентна дифференцируемости на множестве.

LaTeX

$$AnalyticOn ℂ f s ↔ DifferentiableOn ℂ f s$$

Lean4

theorem _root_.DifferentiableOn.analyticOnNhd {s : Set ℂ} {f : ℂ → E} (hd : DifferentiableOn ℂ f s) (hs : IsOpen s) :
    AnalyticOnNhd ℂ f s := fun _z hz => hd.analyticAt (hs.mem_nhds hz)

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