hasFPowerSeriesAt — Mathlib

English

If two functions agree on a ball, the finite power-series-on-ball property is preserved under equality of values.

Русский

Если две функции совпадают на шаре, то свойство конечного ряда сохраняется при равенстве значений.

LaTeX

$$HasFiniteFPowerSeriesOnBall f p x n r → EqOn f g (EMetric.ball x r) → HasFiniteFPowerSeriesOnBall g p x n r$$

Lean4

theorem hasFPowerSeriesAt (hf : HasFiniteFPowerSeriesAt f p x n) : HasFPowerSeriesAt f p x :=
  let ⟨r, hf⟩ := hf
  ⟨r, hf.toHasFPowerSeriesOnBall⟩

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