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