English
If f is eventually bounded above along l and f(x) · g(x) tends to +∞ along l, then g(x) tends to +∞ along l.
Русский
Если f вдоль l ограничено сверху (наступает предел), и произведение f(x)·g(x) стремится к +∞, то g(x) стремится к +∞ вдоль l.
LaTeX
$$$\\text{IsBoundedUnder}(\\le, l, f) \\land \\operatorname{Tendsto}(\\lambda x. f(x) \\cdot g(x))\\ l\\ atTop \\Rightarrow \\operatorname{Tendsto} g\\ l\\ atTop$$$
Lean4
/-- If `f` is eventually bounded from above along `l` and `f * g` tends to `+∞`,
then `g` tends to `+∞`. -/
@[to_additive /-- If `f` is eventually bounded from above along `l` and `f + g` tends to `+∞`,
then `g` tends to `+∞`. -/
]
theorem atTop_of_isBoundedUnder_le_mul (hf : IsBoundedUnder (· ≤ ·) l f) (hfg : Tendsto (fun x => f x * g x) l atTop) :
Tendsto g l atTop := by
obtain ⟨C, hC⟩ := hf
refine .atTop_of_const_mul C <| tendsto_atTop_mono' l ?_ hfg
exact (eventually_map.mp hC).mono fun _ ↦ (mul_le_mul_right' · _)
