atBot_mul_atTop₀ — Mathlib

English

If f tends to −∞ and g tends to +∞, then their product tends to −∞.

Русский

Если f стремится к −∞, а g к +∞, то произведение f g стремится к −∞.

LaTeX

$$$ \text{If } f_l \to -\infty,\ g_l \to +\infty, \ then } fg \to -\infty. $$$

Lean4

theorem atBot_mul_atTop₀ (hf : Tendsto f l atBot) (hg : Tendsto g l atTop) : Tendsto (fun x => f x * g x) l atBot :=
  by
  have : Tendsto (fun x => -f x * g x) l atTop := (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop₀ hg
  simpa only [Function.comp_def, neg_mul_eq_neg_mul, neg_neg] using tendsto_neg_atTop_atBot.comp this

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