sub — Mathlib

English

If HasFPowerSeriesAt holds for f with pf at x and for g with pg at x, then f − g has a local power series at x with coefficients pf − pg.

Русский

Если для функций f и g существует формальное локальное разложение в точке x с коэффициентами pf и pg, то их разность f − g имеет локальное разложение в x с коэффициентами pf − pg.

LaTeX

$$$\text{HasFPowerSeriesAt}(f, pf, x) \land \text{HasFPowerSeriesAt}(g, pg, x) \Rightarrow \text{HasFPowerSeriesAt}(f - g, pf - pg, x)$$$

Lean4

theorem sub (hf : HasFPowerSeriesAt f pf x) (hg : HasFPowerSeriesAt g pg x) : HasFPowerSeriesAt (f - g) (pf - pg) x :=
  by simpa only [sub_eq_add_neg] using hf.add hg.neg

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