fun_prod — Mathlib

English

Let ι be a type, s a finite set of ι, and f: ι → (𝕜 → 𝕜). If each fσ is meromorphic at x, then the function z ↦ ∏ n∈s f n z is meromorphic at x.

Русский

Пусть ι — множество, s — конечное множество из ι, и f: ι → (𝕜 → 𝕜). Если каждая fσ мероморфна в x, то функция z ↦ ∏ n∈s f n z мероморфна в x.

LaTeX

$$$(∀ \\sigma, MeromorphicAt (f \\sigma) x) \\Rightarrow MeromorphicAt (fun z \\mapsto \\prod n \\in s, f n z) x$$$

Lean4

/-- Finite products of meromorphic functions are analytic. -/
@[fun_prop]
theorem fun_prod {ι : Type*} {s : Finset ι} {f : ι → 𝕜 → 𝕜} {x : 𝕜} (h : ∀ σ, MeromorphicAt (f σ) x) :
    MeromorphicAt (fun z ↦ ∏ n ∈ s, f n z) x := by
  convert prod h (s := s)
  simp

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