English
In a linearly ordered commutative group with the order topology, if f converges to C and g tends to atTop, then f g tends to atTop.
Русский
В линейно упорядоченной коммутативной группе с порядковой топологией произведение функций, сходящихся к C и к бесконечности, сходится к бесконечности.
LaTeX
$$$$\operatorname{Tendsto} f\, l\, (nhds C) \land \operatorname{Tendsto} g\, l\, atTop \;\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 `atTop` then `f * g` tends to `atTop`. -/
@[to_additive add_atTop /-- In a linearly ordered additive commutative group with the order
topology, if `f` tends to `C` and `g` tends to `atTop` then `f + g` tends to `atTop`. -/
]
theorem mul_atTop' {C : α} (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atTop :=
by
nontriviality α
obtain ⟨C', hC'⟩ : ∃ C', C' < C := exists_lt C
refine tendsto_atTop_mul_left_of_le' _ C' ?_ hg
exact (hf.eventually (lt_mem_nhds hC')).mono fun x => le_of_lt
