Theorems · Theorem · sequences and series

Filter.Tendsto.den

∀ {α : Type u_4} {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : TopologicalSpace K] [OrderTopology K] [ContinuousInv K] {f g : α → K} {l : Filter α},
  Filter.Tendsto f l Filter.atTop →
    ∀ {a : K}, 0 < a → Filter.Tendsto (fun x => f x / g x) l (nhds a) → Filter.Tendsto g l Filter.atTop

If when x tends to ∞, g tends to ∞ and f x / g x tends to a positive constant, then f tends to ∞.

Defined in

Mathlib.Analysis.SpecificLimits.Basic

Cited by

1 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderIsStrictOrderedRingTopologicalSpaceOrderTopologyContinuousInv