𝕜 : Type u_1
E : Type u_2
inst✝¹ : NormedField 𝕜
inst✝ : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝[{a}ᶜ] a) (norm ∘ f)
⊢ Tendsto (norm ∘ fun x => (x - a)⁻¹) (𝓝[{a}ᶜ] a) atTop
𝕜 : Type u_1
E : Type u_2
inst✝¹ : NormedField 𝕜
inst✝ : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝[{a}ᶜ] a) (norm ∘ f)
⊢ f =o[𝓝[{a}ᶜ] a] fun x => (x - a)⁻¹
refine' (h.isBigO_const (one_ne_zero' ℝ)).trans_isLittleO (isLittleO_const_left.2 <| Or.inr _)
no goals
𝕜 : Type u_1
E : Type u_2
inst✝¹ : NormedField 𝕜
inst✝ : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun x x_1 => x ≤ x_1) (𝓝[{a}ᶜ] a) (norm ∘ f)
⊢ Tendsto (fun x => ‖x - a‖⁻¹) (𝓝[{a}ᶜ] a) atTop
exact (tendsto_norm_sub_self_punctured_nhds a).inv_tendsto_zero