tendsto_atBot_of_add_bdd_below_right'

English

In additive monoids, if f is bounded below and f(x) + g(x) → −∞, then g(x) → −∞.

Русский

В аддитивных моноидах, если f ограничено снизу и f(x) + g(x) → −∞, то g(x) → −∞.

LaTeX

$$$\\text{IsBoundedUnder}(\\ge, l, f) \\land \\operatorname{Tendsto}(f(x) + g(x))\\ l atBot \\Rightarrow \\operatorname{Tendsto} g\\ l atBot$$$

Lean4

@[deprecated Tendsto.atBot_of_add_isBoundedUnder_ge (since := "2025-02-13")]
theorem tendsto_atBot_of_add_bdd_below_right' (C) (hC : ∀ᶠ x in l, C ≤ g x) (h : Tendsto (fun x => f x + g x) l atBot) :
    Tendsto f l atBot :=
  h.atBot_of_add_isBoundedUnder_ge ⟨C, hC⟩

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