toMeromorphicNFOn_of_not_meromorphicOn

English

If f is not meromorphic on U, then the normal-form on U is identically zero.

Русский

Если f не мероморфна на U, то нормальная форма на U тождественно нуль.

LaTeX

$$$\neg MeromorphicOn\ f\ U \Rightarrow toMeromorphicNFOn\ f\ U = 0$$$

Lean4

/-- If `f` is not meromorphic on `U`, conversion to normal form  maps the function
to `0`.
-/
@[simp]
theorem toMeromorphicNFOn_of_not_meromorphicOn (hf : ¬MeromorphicOn f U) : toMeromorphicNFOn f U = 0 := by
  simp [toMeromorphicNFOn, hf]

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