atBot_mul_atBot₀ — Mathlib

English

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

Русский

Если оба бейсового направления функции стремятся к −∞, то их произведение стремится к +∞.

LaTeX

$$$ f_l \to -\infty,\ g_l \to -\infty \Rightarrow f_l g_l \to +\infty. $$$

Lean4

theorem atBot_mul_atBot₀ (hf : Tendsto f l atBot) (hg : Tendsto g l atBot) : Tendsto (fun x => f x * g x) l atTop :=
  by
  have : Tendsto (fun x => -f x * -g x) l atTop :=
    (tendsto_neg_atBot_atTop.comp hf).atTop_mul_atTop₀ (tendsto_neg_atBot_atTop.comp hg)
  simpa only [neg_mul_neg] using this

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