analyticOn_iff_differentiableOn — Mathlib

English

For an open set, analyticOn is equivalent to differentiableOn.

Русский

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

LaTeX

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

Lean4

/-- On an open set, `f : ℂ → E` is analytic iff it is differentiable -/
theorem analyticOn_iff_differentiableOn {f : ℂ → E} {s : Set ℂ} (o : IsOpen s) :
    AnalyticOn ℂ f s ↔ DifferentiableOn ℂ f s :=
  by
  rw [o.analyticOn_iff_analyticOnNhd]
  exact analyticOnNhd_iff_differentiableOn o

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