English
If f tends to ∞, and a>0 is a limit of f/g, then g also tends to ∞; more precisely, asymptotically f/g converges to a positive a implies f and g have the same infinity behavior.
Русский
Если отношение f/g tends к положительному a, то f и g имеют одинаковое бесконечное поведение; в частности, если f→∞, то g→∞.
LaTeX
$$$$ \\text{If } f \\to \\infty, \\; g \\to \\infty, \\; \\frac{f}{g} \\to a>0 \\Rightarrow g \\to \\infty.$$$$
Lean4
/-- If when `x` tends to `∞`, `g` tends to `∞` and `f x / g x` tends to a positive
constant, then `f` tends to `∞`. -/
theorem num {α K : Type*} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [TopologicalSpace K] [OrderTopology K]
{f g : α → K} {l : Filter α} (hg : Tendsto g l atTop) {a : K} (ha : 0 < a)
(hlim : Tendsto (fun x => f x / g x) l (𝓝 a)) : Tendsto f l atTop :=
(hlim.pos_mul_atTop ha hg).congr' (EventuallyEq.div_mul_cancel_atTop hg)
