continuous — Mathlib

English

If an analytic function is analytic everywhere in a neighborhood of x, then it is continuous on that neighborhood.

Русский

Если функция аналитична в окрестности точки x, то она непрерывна на этой окрестности.

LaTeX

$$$ AnalyticOnNhd 𝕜 f univ \Rightarrow Continuous f $$$

Lean4

/-- Analytic everywhere implies continuous -/
theorem continuous {f : E → F} (fa : AnalyticOnNhd 𝕜 f univ) : Continuous f := by rw [← continuousOn_univ];
  exact fa.continuousOn

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