Theorems · Definition · complex analysis

MeromorphicNFOn

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → Set 𝕜 → Prop

A function is 'meromorphic in normal form' on U if has normal form at every point of U.

Defined in

Mathlib.Analysis.Meromorphic.NormalForm

Cited by

35 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace