English
A finite sum of analyticOnNhd functions is analyticOnNhd.
Русский
Конечная сумма аналитических на окрестности функций аналитична на окрестности.
LaTeX
$$$\forall N\,\text{Finset},\ (\forall n\in N,\ AnalyticOnNhd_{\mathfrak k}(f(n),s))\Rightarrow AnalyticOnNhd_{\mathfrak k}\bigl(\lambda z. \sum_{n\in N} f(n)(z)\bigr),s.$$$
Lean4
/-- Finite sums of analytic functions are analytic -/
theorem analyticOnNhd_fun_sum {f : α → E → F} {s : Set E} (N : Finset α) (h : ∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) :
AnalyticOnNhd 𝕜 (fun z ↦ ∑ n ∈ N, f n z) s := fun z zs ↦ N.analyticAt_fun_sum (fun n m ↦ h n m z zs)