tendsto_atTop_of_add_bdd_above_left

English

Again, if f is bounded above along l and f(x) · g(x) → +∞ along l, then g(x) → +∞ along l.

Русский

Ещё раз: если f ограничено сверху вдоль l и f(x)·g(x) → +∞, то g(x) → +∞ вдоль l.

LaTeX

$$$\\text{IsBoundedUnder}(\\le, l, f) \\land \\operatorname{Tendsto}(f(x) \\cdot g(x))\\ l\\ atTop \\Rightarrow \\operatorname{Tendsto} g\\ l\\ atTop$$$

Lean4

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

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