no goals
α : Type ?u.66801
β : Type ?u.66804
γ : Type ?u.66807
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
xt : x ≠ ⊤
⊢ HasBasis (𝓝 x) (fun x => 0 < x) fun ε => Icc (x - ε) (x + ε)
simpa only [pos_iff_ne_zero] using hasBasis_nhds_of_ne_top' xt