atTop_mul_atBot₀ — Mathlib

English

If f grows to +∞ along a filter and g grows to −∞ along the same filter, then their product f g grows to −∞.

Русский

Если f растет до +∞ по фильтру и g убывает до −∞ по тому же фильтру, то произведение f g растет до −∞.

LaTeX

$$$ \text{If } \operatorname{Tendsto} f_l \mathrm{atTop} \text{ and } \operatorname{Tendsto} g_l \mathrm{atBot}, \ \operatorname{Tendsto}(f g)_{l} \mathrm{atBot}. $$$

Lean4

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

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