continuousWithinAt — Mathlib

English

If f is analytic within s at x, then f is continuous within s at x. This is a restatement of the fact that analyticity implies continuity locally.

Русский

Если функция аналитична на множестве s в точке x, то она непрерывна на s в точке x. Это следствие того, что аналитичность влечет за собой непрерывность в окрестности.

LaTeX

$$$ AnalyticWithinAt 𝕜 f s x \Rightarrow ContinuousWithinAt f s x $$$

Lean4

protected theorem continuousWithinAt (hf : AnalyticWithinAt 𝕜 f s x) : ContinuousWithinAt f s x :=
  hf.continuousWithinAt_insert.mono (subset_insert x s)

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