analyticAt_sum — Mathlib

English

A finite sum of analyticOn functions is analyticOn.

Русский

Конечная сумма аналитических на множестве функций аналитична на множестве.

LaTeX

$$$\forall N\,\text{Finset},\ (\forall n\in N,\ AnalyticOn_{\mathfrak k}(f(n),s))\Rightarrow AnalyticOn_{\mathfrak k}\Bigl(\lambda z. \sum_{n\in N} f(n)(z)\Bigr),s.$$$

Lean4

/-- Finite sums of analytic functions are analytic -/
@[fun_prop]
theorem analyticAt_sum {f : α → E → F} {c : E} (N : Finset α) (h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c) :
    AnalyticAt 𝕜 (∑ n ∈ N, f n) c := by
  convert N.analyticAt_fun_sum h
  simp

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