cpolynomialAt — Mathlib

English

If two functions f and g have finite power-series on ball representations, then their difference has one with combined indices.

Русский

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

LaTeX

$$HasFiniteFPowerSeriesOnBall f pf x n r \land HasFiniteFPowerSeriesOnBall g pg x m r \Rightarrow HasFiniteFPowerSeriesOnBall (f - g) (pf - pg) x (max n m) r$$

Lean4

theorem cpolynomialAt : CPolynomialAt 𝕜 f x :=
  f.hasFiniteFPowerSeriesOnBall.cpolynomialAt_of_mem (by simp only [Metric.emetric_ball_top, Set.mem_univ])

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