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)
@[deprecated RCLike.tendsto_inverse_atTop_nhds_zero_nat]
theorem RCLike.tendsto_inverse_atTop_nhds_0_nat (๐•œ : Type u_1) [RCLike ๐•œ] :
Filter.Tendsto (fun (n : โ„•) => (โ†‘n)โปยน) Filter.atTop (nhds 0)

Alias of RCLike.tendsto_inverse_atTop_nhds_zero_nat.