English
If HasFPowerSeriesWithinOnBall f pf s x r holds, then HasFPowerSeriesWithinOnBall (c • f) (c • pf) s x r holds as well.
Русский
Если есть разложение внутри шара для f pf, то и c·f с pf, масштабированным на c, тоже имеет такое разложение.
LaTeX
$$$\text{HasFPowerSeriesWithinOnBall}(f, pf, s, x, r) \Rightarrow \text{HasFPowerSeriesWithinOnBall}(c \cdot f, c \cdot pf, s, x, r)$$$
Lean4
theorem prod {e : E} {f : E → F} {g : E → G} {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G}
(hf : HasFPowerSeriesAt f p e) (hg : HasFPowerSeriesAt g q e) :
HasFPowerSeriesAt (fun x ↦ (f x, g x)) (p.prod q) e :=
by
rcases hf with ⟨_, hf⟩
rcases hg with ⟨_, hg⟩
exact ⟨_, hf.prod hg⟩
