add — Mathlib

English

If hf and hg are HasFPowerSeriesAt for f and g at a point x, then f+g has HasFPowerSeriesAt with pf+pg at x.

Русский

Если hf и hg — степенные ряды для f и g в точке x, то f+g имеет степенной ряд pf+pg в x.

LaTeX

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

Lean4

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

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