tendsto_atBot_of_add_bdd_below_left

English

Deprecated additive right-bound variant: if g(x) is bounded above and f(x) + g(x) → +∞, then f(x) → +∞.

Русский

Устаревшее: правая граница в аддитивной формулировке.

LaTeX

$$$\\text{Eventually}(g(x) \\le C) \\land \\operatorname{Tendsto}(f(x) + g(x))\\ l\\ atTop \\Rightarrow \\operatorname{Tendsto} f\\ l\\ atTop$$$

Lean4

@[deprecated Tendsto.atBot_of_const_le_add (since := "2025-02-13")]
theorem tendsto_atBot_of_add_bdd_below_left (C) (hC : ∀ x, C ≤ f x) :
    Tendsto (fun x => f x + g x) l atBot → Tendsto g l atBot :=
  .atBot_of_const_le_add ⟨C, hC⟩

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