English
If HasFPowerSeriesAt holds for f with pf at e and for g with qg at e, then f − g has a power series with pf − qg at e.
Русский
Если у f и g есть локальные разложения в точке e с pf и qg, то f − g имеет разложение с pf − qg в e.
LaTeX
$$$\text{HasFPowerSeriesAt}(f, pf, e) \land \text{HasFPowerSeriesAt}(g, qg, e) \Rightarrow \text{HasFPowerSeriesAt}(f - g, pf - qg, e)$$$
Lean4
theorem prod {e : E} {f : E → F} {g : E → G} {s : Set E} {p : FormalMultilinearSeries 𝕜 E F}
{q : FormalMultilinearSeries 𝕜 E G} (hf : HasFPowerSeriesWithinAt f p s e) (hg : HasFPowerSeriesWithinAt g q s e) :
HasFPowerSeriesWithinAt (fun x ↦ (f x, g x)) (p.prod q) s e :=
by
rcases hf with ⟨_, hf⟩
rcases hg with ⟨_, hg⟩
exact ⟨_, hf.prod hg⟩
