English
Equivalent formulation: if there exists c with Tendsto f to c along nhdsWithin x, then meromorphicOrderAt f x ≥ 0.
Русский
Эквивалентно: если существует предел вдоль nhdsWithin x, то порядок неотрицателен.
LaTeX
$$∃ c, Tendsto f (nhdsWithin x) (nhds c) ⇒ 0 ≤ meromorphicOrderAt f x$$
Lean4
/-- A meromorphic function converges to a nonzero limit iff its order is zero. -/
theorem tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero (hf : MeromorphicAt f x) :
(∃ c ≠ 0, Tendsto f (𝓝[≠] x) (𝓝 c)) ↔ meromorphicOrderAt f x = 0 :=
by
rcases eq_or_ne (meromorphicOrderAt f x) 0 with ho | ho
· simp [ho, tendsto_ne_zero_of_meromorphicOrderAt_eq_zero hf ho]
simp only [ne_eq, ho, iff_false, not_exists, not_and]
intro c c_ne hc
rcases ho.lt_or_gt with ho | ho
· apply not_tendsto_atTop_of_tendsto_nhds hc.norm
rw [tendsto_norm_atTop_iff_cobounded]
exact tendsto_cobounded_of_meromorphicOrderAt_neg ho
· apply c_ne
exact tendsto_nhds_unique hc (tendsto_zero_of_meromorphicOrderAt_pos ho)
