sub — Mathlib

English

Analogous to At-level subtraction: f−g has a power series if f and g do.

Русский

Аналогично на уровне точки: если f и g имеют степенной ряд, то f−g имеет ряд.

LaTeX

$$$HasFPowerSeriesAt_f pf x \\land HasFPowerSeriesAt_g pg x \\Rightarrow HasFPowerSeriesAt(f - g, pf - pg, x)$$$

Lean4

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

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