analyticOn_univ_iff_differentiable

English

Let f: C → E be a function with E a complex normed space. Then f is analytic on the entire complex plane if and only if f is differentiable on the entire plane.

Русский

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

LaTeX

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

Lean4

theorem analyticOn_univ_iff_differentiable {f : ℂ → E} : AnalyticOn ℂ f univ ↔ Differentiable ℂ f :=
  by
  rw [analyticOn_univ]
  exact analyticOnNhd_univ_iff_differentiable

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