English
For any 𝕜 with a real-algebra structure, the inverse sequence mapped under the algebra map tends to 0 as n→∞.
Русский
Для 𝕜 с алгебраической структурой над ℝ обратная последовательность под отображением алгебры стремится к 0.
LaTeX
$$$$ \\operatorname{Tendsto}(n \\mapsto (n)^{-1})\\text{ atTop }(0). $$$$
Lean4
/-- If when `x` tends to `∞`, `g` tends to `∞` and `f x / g x` tends to a positive
constant, then `f` tends to `∞`. -/
theorem den {α K : Type*} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [TopologicalSpace K] [OrderTopology K]
[ContinuousInv K] {f g : α → K} {l : Filter α} (hf : Tendsto f l atTop) {a : K} (ha : 0 < a)
(hlim : Tendsto (fun x => f x / g x) l (𝓝 a)) : Tendsto g l atTop :=
have hlim' : Tendsto (fun x => g x / f x) l (𝓝 a⁻¹) :=
by
simp_rw [← inv_div (f _)]
exact Filter.Tendsto.inv (f := fun x => f x / g x) hlim
(hlim'.pos_mul_atTop (inv_pos_of_pos ha) hf).congr' (.div_mul_cancel_atTop hf)
