continuousWithinAt_insert — Mathlib

English

The continuous-within-at lemma for HasFPowerSeriesWithinOnBall.states continuity at the insertion point.

Русский

Лемма о непрерывности внутри на вставке указывает на непрерывность в точке вставки.

LaTeX

$$$\text{continuousWithinAtInsert}$$$

Lean4

protected theorem continuousWithinAt_insert (hf : HasFPowerSeriesWithinAt f p s x) :
    ContinuousWithinAt f (insert x s) x := by
  rcases hf with ⟨r, hr⟩
  apply hr.continuousWithinAt_insert

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