English
In a linearly ordered field with order topology, if f → atTop and g → C with C < 0, then f·g → atBot.
Русский
В линейно упорядоченном поле, если f → +∞ и g → C < 0, то f·g → −∞.
LaTeX
$$$\text{If } f\to +\infty \text{ and } g\to C<0, \; f\cdot g \to -\infty.$$$
Lean4
/-- In a linearly ordered field with the order topology, if `f` tends to `Filter.atTop` and `g`
tends to a negative constant `C` then `f * g` tends to `Filter.atBot`. -/
theorem atTop_mul_neg {C : 𝕜} (hC : C < 0) (hf : Tendsto f l atTop) (hg : Tendsto g l (𝓝 C)) :
Tendsto (fun x => f x * g x) l atBot :=
by
have := hf.atTop_mul_pos (neg_pos.2 hC) hg.neg
simpa only [Function.comp_def, neg_mul_eq_mul_neg, neg_neg] using tendsto_neg_atTop_atBot.comp this
