tendsto_pow_div_pow_atTop_atTop — Mathlib

English

If q < p, then x^p / x^q → ∞ as x → ∞ along the real or field setting; hence tends to atTop.

Русский

Если q < p, то x^p / x^q стремится к бесконечности по мере x → ∞, то есть стремится к atTop.

LaTeX

$$$\operatorname{Tendsto}\left( x \mapsto x^p / x^q \right)_{atTop}\ atTop$$$

Lean4

theorem tendsto_pow_div_pow_atTop_atTop {p q : ℕ} (hpq : q < p) : Tendsto (fun x : 𝕜 => x ^ p / x ^ q) atTop atTop :=
  by
  rw [tendsto_congr' pow_div_pow_eventuallyEq_atTop]
  apply tendsto_zpow_atTop_atTop
  cutsat

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