English
If two functions admit a local formal power series expansion within a set around a point x, with respect to pf and pg, then their difference also admits a local formal power series expansion within the same set around x, with coefficients pf − pg.
Русский
Пусть две функции имеют локальное разложение по формальному степенному ряду внутри множества около точки x, с коэффициентами pf и pg; тогда их разность имеет локальное разложение с коэффициентами pf − pg.
LaTeX
$$$\text{HasFPowerSeriesWithinAt}(f, pf, s, x) \land \text{HasFPowerSeriesWithinAt}(g, pg, s, x) \Rightarrow \text{HasFPowerSeriesWithinAt}(f - g, pf - pg, s, x)$$$
Lean4
theorem sub (hf : HasFPowerSeriesWithinAt f pf s x) (hg : HasFPowerSeriesWithinAt g pg s x) :
HasFPowerSeriesWithinAt (f - g) (pf - pg) s x := by simpa only [sub_eq_add_neg] using hf.add hg.neg
