continuousWithinAt_insert — Mathlib

English

If f is analytic within a set s at x, then f is continuous within the enlarged set insert x s at x. That is, AnalyticWithinAt 𝕜 f s x ⇒ ContinuousWithinAt f (insert x s) x.

Русский

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

LaTeX

$$$ AnalyticWithinAt 𝕜 f s x \Rightarrow ContinuousWithinAt f (insert x s) x $$$

Lean4

protected theorem continuousWithinAt_insert (hf : AnalyticWithinAt 𝕜 f s x) : ContinuousWithinAt f (insert x s) x :=
  let ⟨_, hp⟩ := hf
  hp.continuousWithinAt_insert

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