continuousOn — Mathlib

English

If f is analytic on a set s, then f is continuous on s.

Русский

Если функция аналитична на множестве s, то она непрерывна на s.

LaTeX

$$$ AnalyticOn 𝕜 f s \Rightarrow ContinuousOn f s $$$

Lean4

/-- The sum of a converging power series is continuous in its disk of convergence. -/
protected theorem continuousOn [CompleteSpace F] : ContinuousOn p.sum (EMetric.ball 0 p.radius) :=
  by
  rcases (zero_le p.radius).eq_or_lt with h | h
  · simp [← h, continuousOn_empty]
  · exact (p.hasFPowerSeriesOnBall h).continuousOn

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