← Mathematical handbook

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 𝕜)