no goals
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
l : Filter β
f g : β → α
inst✝ : NoMaxOrder α
⊢ HasBasis (𝓝 0) (fun ε => 0 < ε) fun ε => {b | abs b < ε}
simpa using nhds_basis_abs_sub_lt (0 : α)