sub — Mathlib

English

If f and g both have finite power-series on ball data, then f - g has a finite power-series on ball data with indices max(n, m).

Русский

Если оба имеют конечный степенной ряд на шаре, то разность f - g имеет конечный степенной ряд на шаре с параметром max(n, m).

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 sub (hf : HasFiniteFPowerSeriesOnBall f pf x n r) (hg : HasFiniteFPowerSeriesOnBall g pg x m r) :
    HasFiniteFPowerSeriesOnBall (f - g) (pf - pg) x (max n m) r := by simpa only [sub_eq_add_neg] using hf.add hg.neg

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