HepLean Documentation

Mathlib.Analysis.SpecificLimits.RCLike

A collection of specific limit computations for RCLike #

theorem RCLike.tendsto_inverse_atTop_nhds_zero_nat (๐•œ : Type u_1) [RCLike ๐•œ] :
Filter.Tendsto (fun (n : โ„•) => (โ†‘n)โปยน) Filter.atTop (nhds 0)
theorem RCLike.tendsto_add_mul_div_add_mul_atTop_nhds {๐•œ : Type u_1} [RCLike ๐•œ] (a b c : ๐•œ) {d : ๐•œ} (hd : d โ‰  0) :
Filter.Tendsto (fun (k : โ„•) => (a + c * โ†‘k) / (b + d * โ†‘k)) Filter.atTop (nhds (c / d))