rw [_root_.mem_nhds_iff]
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n x : ℕ∞
s : Set ℕ∞
hx : x ≠ ⊤
⊢ s ∈ 𝓝 x ↔ x ∈ s
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n x : ℕ∞
s : Set ℕ∞
hx : x ≠ ⊤
⊢ (∃ t ⊆ s, IsOpen t ∧ x ∈ t) ↔ x ∈ s