fun_smul — Mathlib

English

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

Русский

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

LaTeX

$$$MeromorphicOn s U \rightarrow MeromorphicOn f U \rightarrow MeromorphicOn (fun z => s z \cdot f z) U$$$

Lean4

theorem fun_smul : MeromorphicOn (fun z ↦ s z • f z) U := fun x hx ↦ (hs x hx).smul (hf x hx)

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