tendsto_atBot_of_add_bdd_below_left'

English

For additive monoids, if f is bounded above and f(x) + g(x) → +∞ along l, then g(x) → +∞ along l.

Русский

Для аддитивных моноидов: если f ограничено сверху и f(x) + g(x) → +∞ вдоль l, то g(x) → +∞ вдоль l.

LaTeX

$$$\\exists C, \\forall x, f(x) \\le C \\land \\operatorname{Tendsto}(f(x) + g(x))\\ l\\ atTop \\Rightarrow \\operatorname{Tendsto} g\\ l\\ atTop$$$

Lean4

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

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