Theorems · Theorem · complex analysis

Meromorphic.exists_meromorphicOrderAt_ne_top_iff_forall

∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {f : 𝕜 → E}, Meromorphic f → ((∃ u, meromorphicOrderAt f u ≠ ⊤) ↔ ∀ (u : 𝕜), meromorphicOrderAt f u ≠ ⊤)

If f is meromorphic function on ℝ or ℂ, then there exists a point where a meromorphic function f has finite order iff f has finite order at every point.

Defined in

Mathlib.Analysis.Meromorphic.RCLike

Cited by

1 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupNormedSpace