analyticOnNhd_univ_iff_differentiable

English

Let f: C → E be a function from the complex plane to a normed space E over C (with E complete). Then f is analytic on every neighborhood in the complex plane if and only if f is differentiable at every point of the plane.

Русский

Пусть f: ℂ → E, где E — полное нормированное комплексное пространство. Тогда f аналитична в любой окрестности точек плоскости ⇔ f дифференцируема в каждой точке плоскости.

LaTeX

$$$$ AnalyticOnNhd_{\\mathbb{C}}(f, \\mathbb{C}) \\;\Longleftrightarrow\\; Differentiable_{\\mathbb{C}}(f). $$$$

Lean4

/-- `f : ℂ → E` is entire iff it's differentiable -/
theorem analyticOnNhd_univ_iff_differentiable {f : ℂ → E} : AnalyticOnNhd ℂ f univ ↔ Differentiable ℂ f :=
  by
  simp only [← differentiableOn_univ]
  exact analyticOnNhd_iff_differentiableOn isOpen_univ

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