Theorems · Definition · complex analysis

MeromorphicOn

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

Meromorphy of a function on a set.

Defined in

Mathlib.Analysis.Meromorphic.Basic

Cited by

141 results in Mathlib

Foundations

Depth 167 from the axioms, rests on 3,376 definitions · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace