continuousOn — Mathlib

English

For any analytic function on a neighborhood of a set, the function is continuous on that neighborhood.

Русский

Для любой аналитической функции на окрестности множества функция непрерывна на этой окрестности.

LaTeX

$$$ AnalyticOnNhd 𝕜 f s \Rightarrow ContinuousOn f s $$$

Lean4

protected theorem continuousOn {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) : ContinuousOn f s := fun x hx =>
  (hf x hx).continuousAt.continuousWithinAt

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