sub — Mathlib

English

If both f and g have finite power-series on ball representations, then their difference has a finite power-series on ball representation with index max(n, m).

Русский

Если у f и g есть конечные представления степенного ряда на шаре, то их разность также имеет конечное представление на шаре.

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

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