analyticWithinAt_sum — Mathlib

English

The sum over a finite index set of analyticWithinAt functions is analyticWithinAt.

Русский

Сумма по конечному индексу аналитических функций внутри множества аналитична внутри множества.

LaTeX

$$$\forall N\,\text{Finset},\ (\forall n\in N,\ analyticWithinAt_{\mathfrak k}(f(n),s,c))\Rightarrow AnalyticWithinAt_{\mathfrak k}\bigl(\lambda z. \sum_{n\in N} f(n)(z)\bigr)\,s,c.$$$

Lean4

/-- Finite sums of analytic functions are analytic -/
theorem analyticWithinAt_sum {f : α → E → F} {c : E} {s : Set E} (N : Finset α)
    (h : ∀ n ∈ N, AnalyticWithinAt 𝕜 (f n) s c) : AnalyticWithinAt 𝕜 (∑ n ∈ N, f n) s c :=
  by
  convert N.analyticWithinAt_fun_sum h
  simp

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