fun_div — Mathlib

English

If s is meromorphic on U and t is meromorphic on U, then the function z ↦ s(z)/t(z) is meromorphic on U.

Русский

Если s и t мероморфны на U, то функция z ↦ s(z)/t(z) мероморфна на U.

LaTeX

$$$\text{MeromorphicOn}(s, U) \land \text{MeromorphicOn}(t, U) \Rightarrow \text{MeromorphicOn}\left(\lambda z. \frac{s(z)}{t(z)}, U\right)$$$

Lean4

theorem fun_div : MeromorphicOn (fun z ↦ s z / t z) U := fun x hx ↦ (hs x hx).div (ht x hx)

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