add — Mathlib

English

If hf and hg are HasFPowerSeriesWithinAt for f and g respectively at s and x with pf and pg, then f+g has a HasFPowerSeriesWithinAt with pf+pg.

Русский

Если hf и hg — соответствующие HasFPowerSeriesWithinAt для функций f и g в точке x на s, тогда f+g имеет степенной ряд внутри области с pf+pg.

LaTeX

$$$HasFPowerSeriesWithinAt_f pf\\ s x \\Rightarrow HasFPowerSeriesWithinAt_g pg\\ s x \\Rightarrow HasFPowerSeriesWithinAt(f+g, pf+pg, s, x)$$$

Lean4

theorem add (hf : HasFPowerSeriesWithinAt f pf s x) (hg : HasFPowerSeriesWithinAt g pg s x) :
    HasFPowerSeriesWithinAt (f + g) (pf + pg) s x :=
  by
  rcases (hf.eventually.and hg.eventually).exists with ⟨r, hr⟩
  exact ⟨r, hr.1.add hr.2⟩

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