English
Let M be an ordered commutative monoid with a compatible order. If f and g are functions from α to M that both tend to +∞ along a filter l, then the pointwise product f(x) · g(x) also tends to +∞ along l.
Русский
Пусть M — упорядоченный коммутативный полукольцо с непрерывной по порядку умножением. Если функции f,g: α → M стремятся к +∞ вдоль фильтра l, то их произведение f(x) · g(x) также стремится к +∞ вдоль l.
LaTeX
$$$\\forall \\alpha \\; \\forall M$, with $M$ a commutative ordered monoid, if $\\operatorname{Tendsto} f\\;l\\;\\atTop$ and $\\operatorname{Tendsto} g\\;l\\;\\atTop$, then $\\operatorname{Tendsto}(\\lambda x. f(x) \\cdot g(x))\\;l\\;\\atTop$.$$
Lean4
/-- In an ordered multiplicative monoid, if `f` and `g` tend to `+∞`, then so does `f * g`.
Earlier, this name was used for a similar lemma about semirings,
which is now called `Filter.Tendsto.atTop_mul_atTop₀`. -/
@[to_additive]
theorem atTop_mul_atTop (hf : Tendsto f l atTop) (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atTop :=
hf.atTop_mul_one_eventuallyLE <| hg.eventually_ge_atTop 1
