tendsto_cobounded_iff_meromorphicOrderAt_neg

English

If meromorphicOrderAt f x < 0, then Tendsto to cobounded; conversely.

Русский

Если порядок f в x меньше нуля, то существует предел в cobounded; и наоборот.

LaTeX

$$$ meromorphicOrderAt\ f\ x < 0 \iff Tendsto\ f\ (nhdsWithin x)\ (cobounded E)$$$

Lean4

/-- A meromorphic function converges to infinity iff its order is negative. -/
theorem tendsto_cobounded_iff_meromorphicOrderAt_neg (hf : MeromorphicAt f x) :
    Tendsto f (𝓝[≠] x) (Bornology.cobounded E) ↔ meromorphicOrderAt f x < 0 :=
  by
  rcases lt_or_ge (meromorphicOrderAt f x) 0 with ho | ho
  · simp [ho, tendsto_cobounded_of_meromorphicOrderAt_neg]
  · simp only [lt_iff_not_ge, ho, not_true_eq_false, iff_false, ← tendsto_norm_atTop_iff_cobounded]
    obtain ⟨c, hc⟩ := tendsto_nhds_of_meromorphicOrderAt_nonneg hf ho
    exact not_tendsto_atTop_of_tendsto_nhds hc.norm

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