English
If f tends to atTop and g tends to C, then their product tends to atTop.
Русский
Если f стремится к бесконечности, а g стремится к конечному значению, то произведение стремится к бесконечности.
LaTeX
$$$$\operatorname{Tendsto} f\, l\, atTop \; \Rightarrow\; \operatorname{Tendsto} g\, l\, (nhds C) \; \Rightarrow\; \operatorname{Tendsto}(x \mapsto f(x) \cdot g(x))\, l\, atTop.$$$$
Lean4
/-- In a linearly ordered commutative group with the order topology,
if `f` tends to `C` and `g` tends to `atBot` then `f * g` tends to `atBot`. -/
@[to_additive add_atBot /-- In a linearly ordered additive commutative group with the order
topology, if `f` tends to `C` and `g` tends to `atBot` then `f + g` tends to `atBot`. -/
]
theorem mul_atBot' {C : α} (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atBot :=
Filter.Tendsto.mul_atTop' (α := αᵒᵈ) hf hg
