Theorems · Theorem · complex analysis

meromorphicOrderAt_finprod_ne_top

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_5} {F : ι → 𝕜 → 𝕜},
  (∀ (c : ι), MeromorphicAt (F c) x) →
    (∀ (c : ι), meromorphicOrderAt (F c) x ≠ ⊤) → meromorphicOrderAt (∏ᶠ (c : ι), F c) x ≠ ⊤

A finprod of functions that do not vanish locally does not vanish locally.

Defined in

Mathlib.Analysis.Meromorphic.Order

Cited by

0 results in Mathlib

Foundations

Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedField