prod — Mathlib

English

Finite products of meromorphic functions are meromorphic on U.

Русский

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

LaTeX

$$$MeromorphicOn (s.prod (fun n => f n)) U \Rightarrow (∀ (n), MeromorphicOn (f n) U) $$MeromorphicOn (s.prod fun n => f n) U$$$

Lean4

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

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