tendsto_nhds_of_meromorphicOrderAt_nonneg

English

If meromorphicOrderAt f x ≥ 0, then f has a limit in the punctured neighborhood of x (nhdsWithin x).

Русский

Если порядок f в x неотрицателен, то функция сходится к пределy в пунктированной окрестности x.

LaTeX

$$$0 \le meromorphicOrderAt\ f\ x \Rightarrow \exists c, Tendsto\ f\ (nhdsWithin x) (nhds c)$$$

Lean4

/-- If the order of a meromorphic function is nonnegative, then this function converges
at this point. See also the iff version `tendsto_nhds_iff_meromorphicOrderAt_nonneg`. -/
theorem tendsto_nhds_of_meromorphicOrderAt_nonneg (hf : MeromorphicAt f x) (ho : 0 ≤ meromorphicOrderAt f x) :
    ∃ c, Tendsto f (𝓝[≠] x) (𝓝 c) := by
  rcases ho.eq_or_lt with ho | ho
  · rcases tendsto_ne_zero_of_meromorphicOrderAt_eq_zero hf ho.symm with ⟨c, -, hc⟩
    exact ⟨c, hc⟩
  · exact ⟨0, tendsto_zero_of_meromorphicOrderAt_pos ho⟩

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