tendsto_pow_div_pow_atTop_zero — Mathlib

English

If p < q, then x^p / x^q → 0 as x → ∞ in a suitable topological field setting.

Русский

Если p < q, то x^p / x^q → 0 при x → ∞ в подходящем поле с топологией.

LaTeX

$$$\operatorname{Tendsto}\left( x \mapsto \dfrac{x^p}{x^q} \right)_{atTop} (\mathcal{N}(0))$$$

Lean4

theorem tendsto_pow_div_pow_atTop_zero [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p q : ℕ} (hpq : p < q) :
    Tendsto (fun x : 𝕜 => x ^ p / x ^ q) atTop (𝓝 0) :=
  by
  rw [tendsto_congr' pow_div_pow_eventuallyEq_atTop]
  apply tendsto_zpow_atTop_zero
  cutsat

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