Theorems · Theorem · complex analysis

meromorphicOrderAt_add_of_ne

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f₁ x →
    MeromorphicAt f₂ x →
      meromorphicOrderAt f₁ x ≠ meromorphicOrderAt f₂ x →
        meromorphicOrderAt (f₁ + f₂) x = min (meromorphicOrderAt f₁ x) (meromorphicOrderAt f₂ x)

If two meromorphic functions have unequal orders, then the order of their sum is exactly the minimum of the orders of the summands.

Defined in

Mathlib.Analysis.Meromorphic.Order

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace