English
If f has finite F-power-series representations on balls around x with radii n and m, then f has a finite power-series on ball with radius max(n,m).
Русский
Если у f есть конечные представления степенного ряда на шарах вокруг x с радиусами n и m, то f имеет конечный степенной ряд на шаре радиуса max(n,m).
LaTeX
$$$ HasFiniteFPowerSeriesAt f pf x n \rightarrow HasFiniteFPowerSeriesAt g pg x m \rightarrow HasFiniteFPowerSeriesAt (f+g) (pf+pg) x (max n m) $$$
Lean4
theorem add (hf : HasFiniteFPowerSeriesAt f pf x n) (hg : HasFiniteFPowerSeriesAt g pg x m) :
HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (max n m) :=
by
rcases (hf.eventually.and hg.eventually).exists with ⟨r, hr⟩
exact ⟨r, hr.1.add hr.2⟩
