analyticOn_prod — Mathlib

English

Finite sums of analyticOnNhd functions are 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 products of analytic functions are analytic -/
theorem analyticOn_prod {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A] {f : α → E → A} {s : Set E} (N : Finset α)
    (h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s) : AnalyticOn 𝕜 (∏ n ∈ N, f n) s := fun z zs ↦
  N.analyticWithinAt_prod (fun n m ↦ h n m z zs)

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