continuousOn — Mathlib

English

The continuous-within-at lemma at the inserted set says continuity at x from within the extended set.

Русский

Лемма о непрерывности внутри в точке вставки гласит непрерывность в x из расширенного множества.

LaTeX

$$$\text{continuousWithinAt_insert}$$$

Lean4

/-- If a function admits a power series expansion within a set on a ball, then it is
continuous there. -/
protected theorem continuousOn (hf : HasFPowerSeriesWithinOnBall f p s x r) :
    ContinuousOn f (insert x s ∩ EMetric.ball x r) :=
  hf.tendstoLocallyUniformlyOn'.continuousOn <|
    Eventually.of_forall fun n => ((p.partialSum_continuous n).comp (continuous_id.sub continuous_const)).continuousOn

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