English
In an ordered multiplicative monoid, if both f and g tend to −∞ along a filter l, then their product f(x) · g(x) also tends to −∞ along l.
Русский
В упорядоченной умножаемой моноиде, если f(x) и g(x) стремятся к −∞ вдоль фильтра l, то и произведение f(x)·g(x) стремится к −∞ вдоль l.
LaTeX
$$$\\forall f,g: \\alpha \\to M,$ with $M$ an ordered commutative monoid, if $\\operatorname{Tendsto} f\\ l\\ atBot$ and $\\operatorname{Tendsto} g\\ l\\ atBot$, then $\\operatorname{Tendsto}(\\lambda x. f(x) \\cdot g(x))\\ l\\ atBot$.$$
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 rings (with conclusion `f * g → +∞`),
which is now called `Filter.Tendsto.atBot_mul_atBot₀`. -/
@[to_additive]
theorem atBot_mul_atBot (hf : Tendsto f l atBot) (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atBot :=
hf.atTop_mul_atTop (M := Mᵒᵈ) hg
