toMeromorphicNFAt_of_not_meromorphicAt

English

If f is not meromorphic at x, then its normal-form value is 0.

Русский

Если f не мероморфна в x, то её нормальная форма равна нулю.

LaTeX

$$$\neg MeromorphicAt\ f\ x \Rightarrow toMeromorphicNFAt\ f\ x = 0$$$

Lean4

/-- If `f` is not meromorphic, conversion to normal form at `x` maps the function to `0`. -/
@[simp]
theorem toMeromorphicNFAt_of_not_meromorphicAt (hf : ¬MeromorphicAt f x) : toMeromorphicNFAt f x = 0 := by
  simp [toMeromorphicNFAt, hf]

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