English
Let a finite family of functions f_n : E → A be analytic on a neighborhood set s. Then the product over n in the finite index set N, ∏_{n∈N} f_n, is analytic on s.
Русский
Пусть для конечного множества индексов N имеется семья функций f_n : E → A, каждая из которых аналитична в окрестности s. Тогда произведение ∏_{n∈N} f_n аналитично в s.
LaTeX
$$$\left(\forall n \in N,\ AnalyticOnNhd 𝕜 (f\,n) s\right) \Rightarrow AnalyticOnNhd 𝕜 (\prod n \in N, f n) s$$$
Lean4
/-- Finite products of analytic functions are analytic -/
theorem analyticOnNhd_prod {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A] {f : α → E → A} {s : Set E} (N : Finset α)
(h : ∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s) : AnalyticOnNhd 𝕜 (∏ n ∈ N, f n) s := fun z zs ↦
N.analyticAt_prod (fun n m ↦ h n m z zs)
