fun_prod — Mathlib

English

Finite products of meromorphic functions are meromorphic on U.

Русский

Конечные произведения мероморфных функций мероморфны на U.

LaTeX

$$$theorem\ MeromorphicOn.fun_prod : (∀ σ, MeromorphicOn (f σ) U) \rightarrow MeromorphicOn (fun z => s.prod (fun n => f n z)) U$$$

Lean4

/-- Finite products of meromorphic functions are analytic. -/
theorem fun_prod {U : Set 𝕜} {ι : Type*} {s : Finset ι} {f : ι → 𝕜 → 𝕜} (h : ∀ σ, MeromorphicOn (f σ) U) :
    MeromorphicOn (fun z ↦ ∏ n ∈ s, f n z) U := fun z hz ↦ MeromorphicAt.fun_prod (fun σ ↦ h σ z hz)

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