tendsto_atTop_of_add_bdd_above_right

English

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

Русский

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

LaTeX

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

Lean4

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

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