atBot_of_mul_const_le — Mathlib

English

A dual formulation: if Tendsto (f(x) · C) to +∞, then Tendsto f to +∞, in the reversed order context.

Русский

Дуальная формулировка: если Tendsto (f(x) · C) → +∞, то Tendsto f → +∞, в контексте обращения порядка.

LaTeX

$$$\\operatorname{Tendsto}(\\lambda x. f(x) \\cdot C)\\ l\\ atTop \\Rightarrow \\operatorname{Tendsto} f\\ l\\ atTop$$$

Lean4

@[to_additive]
theorem atBot_of_mul_const_le (hg : ∃ C, ∀ x, C ≤ g x) (hfg : Tendsto (fun x ↦ f x * g x) l atBot) :
    Tendsto f l atBot :=
  Tendsto.atTop_of_mul_le_const (M := Mᵒᵈ) hg hfg

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