atBot_mul_pos — Mathlib

English

In a linearly ordered field with order topology, if f → atBot and g → 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 `Filter.atBot` and `g`
tends to a positive constant `C` then `f * g` tends to `Filter.atBot`. -/
theorem atBot_mul_pos {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l atBot) (hg : Tendsto g l (𝓝 C)) :
    Tendsto (fun x => f x * g x) l atBot :=
  by
  have := (tendsto_neg_atBot_atTop.comp hf).atTop_mul_pos hC hg
  simpa [Function.comp_def] using tendsto_neg_atTop_atBot.comp this

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