meromorphicNFAt_mem_codiscreteWithin

English

Meromorphic functions have normal form on a codiscrete set inside U whenever they are meromorphic on U.

Русский

У функции мероморфна в нормальной форме на кодискретном подмножестве внутри U, если она мероморфна на U.

LaTeX

$$$\text{MeromorphicNFOn } f U$ implies $\{x : a\;|\; \text{MeromorphicNFAt } f x\} \in \text{Filter.codiscreteWithin } U$$$

Lean4

/-- Meromorphic functions have normal form outside of a discrete subset in the domain of
meromorphicity. -/
theorem meromorphicNFAt_mem_codiscreteWithin {U : Set 𝕜} (hf : MeromorphicOn f U) :
    {x | MeromorphicNFAt f x} ∈ Filter.codiscreteWithin U :=
  by
  filter_upwards [hf.analyticAt_mem_codiscreteWithin] with _ ha
  exact ha.meromorphicNFAt

Похожие утверждения