continuousWithinAt — Mathlib

English

Let f: E → F admit a formal power series expansion f ≈ p around x on a set s. Then f is continuous at x when restricted to s; that is, f is ContinuousWithinAt f s x.

Русский

Пусть f: E → F имеет формальное разложение по степенному ряду вокруг точки x на множестве s. Тогда эта функция непрерывна в точке x при ограничении на s; то есть ContinuousWithinAt f s x.

LaTeX

$$$ HasFPowerSeriesWithinAt f p s x \Rightarrow ContinuousWithinAt f s x $$$

Lean4

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

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