English
If f and g have power series within ball with radii r and r' on s at x, then f−g has a power series within ball with radii r at x.
Русский
Если f и g имеют степенные ряды внутри шара радиусов r и r' на s в точке x, то разность f−g имеет ряд внутри шара.
LaTeX
$$$HasFPowerSeriesWithinOnBall(f pf\\ s x r) \\land HasFPowerSeriesWithinOnBall(g pg\\ s x r) \\Rightarrow HasFPowerSeriesWithinOnBall(f-g, pf-pg, s, x, r)$$$
Lean4
theorem add (hf : HasFPowerSeriesOnBall f pf x r) (hg : HasFPowerSeriesOnBall g pg x r) :
HasFPowerSeriesOnBall (f + g) (pf + pg) x r :=
{ r_le := le_trans (le_min_iff.2 ⟨hf.r_le, hg.r_le⟩) (pf.min_radius_le_radius_add pg)
r_pos := hf.r_pos
hasSum := fun hy => (hf.hasSum hy).add (hg.hasSum hy) }
