English
If C is a fixed element and C · f(x) tends to +∞ along l, then f(x) tends to +∞ along l, in a cancellative ordered monoid.
Русский
Если фиксированное C удовлетворяет $C\\cdot f(x)\\to +\\infty$, то $f(x)\\to +\\infty$ вдоль l, в упорядоченном cancelar-монойде.
LaTeX
$$$\\operatorname{Tendsto}(\\lambda x. C \\cdot f(x))\\ l\\ atTop \\Rightarrow \\operatorname{Tendsto} f\\ l\\ atTop$$$
Lean4
/-- In an ordered cancellative multiplicative monoid, if `C * f x → +∞`, then `f x → +∞`.
Earlier, this name was used for a similar lemma about ordered rings,
which is now called `Filter.Tendsto.atTop_of_const_mul₀`. -/
@[to_additive]
theorem atTop_of_const_mul (C : M) (hf : Tendsto (C * f ·) l atTop) : Tendsto f l atTop :=
tendsto_atTop.2 fun b ↦ (tendsto_atTop.1 hf (C * b)).mono fun _ ↦ le_of_mul_le_mul_left'
