English
A finite product of analyticAt functions is analyticAt.
Русский
Конечный произведение аналитических в точке функций аналитично в точке.
LaTeX
$$$\forall N\,\text{Finset},\ (\forall n\in N,\ AnalyticAt_{\mathfrak k}(f(n),c))\Rightarrow AnalyticAt_{\mathfrak k}\bigl(\prod_{n\in N} f(n)\bigr)(c).$$$
Lean4
/-- Finite products of analytic functions are analytic -/
theorem analyticWithinAt_fun_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 𝕜 (fun z ↦ ∏ n ∈ N, f n z) s c := by
classical
induction N using Finset.induction with
| empty =>
simp only [Finset.prod_empty]
exact analyticWithinAt_const
| insert a B aB hB =>
simp_rw [Finset.prod_insert aB]
simp only [Finset.mem_insert] at h
exact (h a (Or.inl rfl)).mul (hB fun b m ↦ h b (Or.inr m))
