atTop_of_mul_isBoundedUnder_le — Mathlib

English

See item 158265; a duplicate formulation for g tending to +∞ when f is bounded above and f·g→∞.

Русский

См. п. 158265; повторная формулировка для стремления g к +∞ при ограниченности f сверху и f·g→∞.

LaTeX

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

Lean4

@[to_additive]
theorem atTop_of_mul_isBoundedUnder_le (hg : IsBoundedUnder (· ≤ ·) l g) (h : Tendsto (fun x => f x * g x) l atTop) :
    Tendsto f l atTop := by
  obtain ⟨C, hC⟩ := hg
  refine .atTop_of_mul_const C <| tendsto_atTop_mono' l ?_ h
  exact (eventually_map.mp hC).mono fun _ ↦ (mul_le_mul_left' · _)

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