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 ∧ r' on s at x.
Русский
Если f и g имеют степенные ряды внутри шара радиусов r и r' на s в точке x, то сумма f+g имеет степенной ряд внутри шара радиуса r ∧ r' в x.
LaTeX
$$$\\text{HasFPowerSeriesWithinOnBall}(f pf\\ s x r) \\land \\text{HasFPowerSeriesWithinOnBall}(g pg\\ s x r) \\Rightarrow \\text{HasFPowerSeriesWithinOnBall}(f+g, pf+pg, s, x, \\min(r, r'))$$$
Lean4
theorem add (hf : HasFPowerSeriesWithinOnBall f pf s x r) (hg : HasFPowerSeriesWithinOnBall g pg s x r) :
HasFPowerSeriesWithinOnBall (f + g) (pf + pg) s 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 h'y => (hf.hasSum hy h'y).add (hg.hasSum hy h'y) }
