analyticAt_prod — Mathlib

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 -/
@[fun_prop]
theorem analyticAt_prod {α : Type*} {A : Type*} [NormedCommRing A] [NormedAlgebra 𝕜 A] {f : α → E → A} {c : E}
    (N : Finset α) (h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c) : AnalyticAt 𝕜 (∏ n ∈ N, f n) c :=
  by
  convert N.analyticAt_fun_prod h
  simp

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