pos_mul_atBot — Mathlib

English

If a function tends to atTop, then its negation tends to atBot; if a function tends to atBot, its negation tends to atTop.

Русский

Если функция стремится к +∞, то её отрицание к −∞, и наоборот.

LaTeX

$$$\text{If } f\to +\infty, \; -f\to -\infty; \text{ conversely: } f\to -\infty, \; -f\to +\infty.$$$

Lean4

/-- In a linearly ordered field with the order topology, if `f` tends to a positive constant `C` and
`g` tends to `Filter.atBot` then `f * g` tends to `Filter.atBot`. -/
theorem pos_mul_atBot {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l (𝓝 C)) (hg : Tendsto g l atBot) :
    Tendsto (fun x => f x * g x) l atBot := by simpa only [mul_comm] using hg.atBot_mul_pos hC hf

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