tendsto_div_const_atTop_of_pos — Mathlib

English

If r > 0 and f tends to infinity along l, then f(x)/r tends to infinity along l, equivalently to f(x) tends to infinity along l.

Русский

Если r > 0 и f идёт к бесконечности вдоль l, то f(x)/r идёт к бесконечности вдоль l (и наоборот).

LaTeX

$$$\text{Tendsto}(f/l)\ l\ atTop \iff 0

Lean4

/-- If `r` is a positive constant, `x ↦ f x / r` tends to infinity along a filter
if and only if `f` tends to infinity along the same filter. -/
theorem tendsto_div_const_atTop_of_pos (hr : 0 < r) : Tendsto (fun x ↦ f x / r) l atTop ↔ Tendsto f l atTop := by
  simpa only [div_eq_mul_inv] using tendsto_mul_const_atTop_of_pos (inv_pos.2 hr)

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