meromorphicOn — Mathlib

English

If a function is meromorphic in normal form on U, then it is meromorphic on U.

Русский

Если функция мероморфна в нормальной форме на U, то она мероморфна на U.

LaTeX

$$$MeromorphicNFOn\ f\ U \Rightarrow MeromorphicOn\ f\ U$$$

Lean4

/-- If a function is meromorphic in normal form on `U`, then it is meromorphic on
`U`.
-/
theorem meromorphicOn (hf : MeromorphicNFOn f U) : MeromorphicOn f U := fun _ hz ↦ (hf hz).meromorphicAt

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