English
If every fσ is meromorphic at x for σ in ι, then the finite product ∏ n∈s f n is meromorphic at x.
Русский
Если для каждого σ из ι функция fσ мероморфна в x, то конечное произведение ∏ σ∈s fσ мероморфно в x.
LaTeX
$$$\\forall \\sigma,\, MeromorphicAt (f \\sigma) x \\;\\Rightarrow\\; MeromorphicAt (\\prod n \\in s, f n) x$$$
Lean4
/-- Finite products of meromorphic functions are analytic. -/
@[fun_prop]
theorem prod {ι : Type*} {s : Finset ι} {f : ι → 𝕜 → 𝕜} {x : 𝕜} (h : ∀ σ, MeromorphicAt (f σ) x) :
MeromorphicAt (∏ n ∈ s, f n) x := by
classical
induction s using Finset.induction with
| empty =>
rw [Finset.prod_empty]
exact analyticAt_const.meromorphicAt
| insert σ s hσ hind =>
rw [Finset.prod_insert hσ]
exact (h σ).mul hind
