neg_mul_atTop — Mathlib

English

In a linearly ordered field, if f → atBot and g → C with C > 0, then f·g → atTop.

Русский

Если 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 a negative constant `C` and
`g` tends to `Filter.atTop` then `f * g` tends to `Filter.atBot`. -/
theorem neg_mul_atTop {C : 𝕜} (hC : C < 0) (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x * g x) l atBot := by simpa only [mul_comm] using hg.atTop_mul_neg hC hf

Похожие утверждения