analyticWithinAt_prod — Mathlib

English

A finite product of analyticWithinAt functions is analyticWithinAt.

Русский

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

LaTeX

$$$\forall N\,\text{Finset},\ (\forall n\in N,\ AnalyticWithinAt_{\mathfrak k}(f(n),s,x))\Rightarrow AnalyticWithinAt_{\mathfrak k}\Bigl(\prod_{n\in N} f(n)\Bigr)(s,x).$$$

Lean4

/-- Finite products of analytic functions are analytic -/
theorem analyticWithinAt_prod {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A] {f : α → E → A} {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_prod h
  simp

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