English
If f tends to atTop and g tends to nhds C, then f g tends to atTop.
Русский
Если f стремится к бесконечности, а g стремится к некоторому C, то произведение стремится к бесконечности.
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 `atTop` and `g` tends to `C` then `f * g` tends to `atTop`. -/
@[to_additive atTop_add /-- In a linearly ordered additive commutative group with the order
topology, if `f` tends to `atTop` and `g` tends to `C` then `f + g` tends to `atTop`. -/
]
theorem atTop_mul' {C : α} (hf : Tendsto f l atTop) (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atTop :=
by
conv in _ * _ => rw [mul_comm]
exact hg.mul_atTop' hf
