α : Type u_2
β : Type u_1
inst✝ : NormedAddCommGroup β
l : Filter α
f : α → β
hf : f =o[l] fun _x => 1
⊢ BoundedAtFilter l f
α : Type u_2
β : Type u_1
inst✝ : NormedAddCommGroup β
l : Filter α
f : α → β
hf : ZeroAtFilter l f
⊢ BoundedAtFilter l f
rw [ZeroAtFilter, ← Asymptotics.isLittleO_const_iff (one_ne_zero' ℝ)] at hf
no goals
α : Type u_2
β : Type u_1
inst✝ : NormedAddCommGroup β
l : Filter α
f : α → β
hf : f =o[l] fun _x => 1
⊢ BoundedAtFilter l f
exact hf.isBigO