num_atTop_iff_den_atTop — Mathlib

English

For any positive r, the sequence (r+1)^n tends to infinity as n grows.

Русский

Для любого положительного r последовательность (r+1)^n растёт без границы при возрастании n.

LaTeX

$$$$ \\lim_{n\\to\\infty} (r+1)^n = \\infty \\quad (r>0). $$$$

Lean4

/-- If when `x` tends to `∞`, `f x / g x` tends to a positive constant, then `f` tends to `∞` if
  and only if `g` tends to `∞`. -/
theorem num_atTop_iff_den_atTop {α K : Type*} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [TopologicalSpace K]
    [OrderTopology K] [ContinuousInv K] {f g : α → K} {l : Filter α} {a : K} (ha : 0 < a)
    (hlim : Tendsto (fun x => f x / g x) l (𝓝 a)) : Tendsto f l atTop ↔ Tendsto g l atTop :=
  ⟨fun hf ↦ hf.den ha hlim, fun hg ↦ hg.num ha hlim⟩

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