English
In a linearly ordered group with order topology, if f tends to atBot and g tends to C, then f g tends to atBot.
Русский
В группе с порядком и топологией, если f стремится к минус бесконечности, а g к C, то произведение стремится к минус бесконечности.
LaTeX
$$$$\operatorname{Tendsto} f\, l\, atBot \rightarrow \operatorname{Tendsto} g\, l\, (nhds C) \rightarrow \operatorname{Tendsto}(x \mapsto f(x) \cdot g(x))\, l\, atBot.$$$$
Lean4
/-- In a linearly ordered commutative group with the order topology,
if `f` tends to `atBot` and `g` tends to `C` then `f * g` tends to `atBot`. -/
@[to_additive atBot_add /-- In a linearly ordered additive commutative group with the order
topology, if `f` tends to `atBot` and `g` tends to `C` then `f + g` tends to `atBot`. -/
]
theorem atBot_mul' {C : α} (hf : Tendsto f l atBot) (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atBot :=
by
conv in _ * _ => rw [mul_comm]
exact hg.mul_atBot' hf
