A collection of specific limit computations for RCLike

theorem RCLike.tendsto_ofReal_cobounded_cobounded (𝕜 : Type u_1) [RCLike 𝕜] : Filter.Tendsto ofReal (Bornology.cobounded ℝ) (Bornology.cobounded 𝕜)

theorem RCLike.tendsto_ofReal_atTop_cobounded (𝕜 : Type u_1) [RCLike 𝕜] : Filter.Tendsto ofReal Filter.atTop (Bornology.cobounded 𝕜)

theorem RCLike.tendsto_ofReal_atBot_cobounded (𝕜 : Type u_1) [RCLike 𝕜] : Filter.Tendsto ofReal Filter.atBot (Bornology.cobounded 𝕜)

@[deprecated tendsto_inv_atTop_nhds_zero_nat (since := "2025-10-27")]

theorem RCLike.tendsto_inverse_atTop_nhds_zero_nat {𝕜 : Type u_4} [DivisionSemiring 𝕜] [CharZero 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)

Alias of tendsto_inv_atTop_nhds_zero_nat.

@[deprecated tendsto_add_mul_div_add_mul_atTop_nhds (since := "2025-10-27")]

theorem RCLike.tendsto_add_mul_div_add_mul_atTop_nhds {𝕜 : Type u_4} [Semifield 𝕜] [CharZero 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] [IsTopologicalSemiring 𝕜] [ContinuousInv₀ 𝕜] (a b c : 𝕜) {d : 𝕜} (hd : d ≠ 0) : Filter.Tendsto (fun (k : ℕ) => (a + c * ↑k) / (b + d * ↑k)) Filter.atTop (nhds (c / d))

Alias of tendsto_add_mul_div_add_mul_atTop_nhds.