neg_mul_atBot — Mathlib

English

In a linearly ordered field with order topology, 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.atBot` then `f * g` tends to `Filter.atTop`. -/
theorem neg_mul_atBot {C : 𝕜} (hC : C < 0) (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atBot) :
    Tendsto (fun x => f x * g x) l atTop := by simpa only [mul_comm] using hg.atBot_mul_neg hC hf

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